Search papers, labs, and topics across Lattice.
This paper introduces KS-CFA, a novel control-flow attestation scheme that effectively detects control-flow bending (CFB) attacks without the significant drawbacks of existing methods. By leveraging symbolic execution and focusing on input-sourced control-flow dependent variables, KS-CFA enables the verification of program execution across various transfer types without the need for extensive measurement spaces or low-level hardware modifications. The implementation on RISC-V Keystone TEE shows that while there is a prover-side overhead of 6.7-32.2x, the solution offers a robust defense against CFB attacks with efficient verification processes.
KS-CFA can detect sophisticated control-flow bending attacks without the heavy overhead of traditional methods, making it a game-changer for secure program execution verification.
Control-flow attestation (CFA) enables a remote entity to verify program execution on a target device by monitoring control-flow behaviour at runtime. However, control-flow bending (CFB) attacks remain difficult to detect, where an adversary steers execution along legal edges of the program's control-flow graph by corrupting branch flags, loop counters, and other runtime data. Existing solutions impose significant drawbacks: they require enumerating vast measurement spaces, cover only a reduced subset of attacks, or rely on low-level hardware modifications. In this work, we present KS-CFA, a new CFA scheme that detects CFB attacks across four transfer types (indirect calls, conditional and indirect jumps, and returns) without those costs. To this end, we combine symbolic execution and selective identification of input-sourced control-flow dependent variables: a strict subset of control-flow-relevant state whose values are directly read from external input. The proving device records, inside a trusted execution environment (TEE), a control-flow trace and the external inputs that determine relevant run-time variables. The verifier then replays the reported path through single-path symbolic execution, predicting each transfer and localising divergences that signal an attack. We implement and evaluate KS-CFA using the RISC-V Keystone TEE and Embench-IoT on QEMU and a Rocket-based FPGA platform (NiteFury II). Prover-side overhead relative to unattested execution ranges from 6.8-20.5x on QEMU and 6.7-32.2x on the FPGA, and verification requires no path or value enumeration.
