Control-flow integrity for resource-constrained devices

Control-Flow Integrity (CFI) ensures that an attacker cannot tamper with the execution logic of a program, e.g., by reusing its code to implement malicious operations. In the past, several attacks have actively exploited CFI failures for hijacking the control logic of programs. Although enforcing the CFI of programs is a significant concern, implementing effective control mechanisms is highly complex. Although often control-flow properties are regarded as practically enforceable, as most languages include data-driven branch operators, CFI is, in fact, also a data-flow property. Furthermore, when the execution platform supports any sort of non-determinism, e.g., think of program interrupts, static models for CFI analysis, such as control-flow graphs (CFG), cannot be accurately computed. Thus, it is not surprising that CFI is often only partially guaranteed by means of weaker security models. In this paper, we present a novel CFI enforcement framework for dealing with the aforementioned issues. Like other proposals, our method relies on code instrumentation for deploying CFI checks among the instructions of a target program. However, our policy enforcement framework also monitors interrupt routines to ensure that the attacker cannot exploit them. Finally, we provide our proposal with formal semantics that we use to provide the correctness of our solution.