EMSOFT’16, October 01-07, 2016, Pittsburgh, PA, USA.
Jiaqi Tan, Hui Jun Tay, Utsav Drolia, Rajeev Gandhi, Priya Narasimhan
Deptartment of Electrical and Computer Engineering
Carnegie Mellon University
Control-Flow Integrity (CFI) is an important safety property of software, particularly in embedded and safety-critical systems, where CFI violations have led to patient deaths and can render cars remotely controllable by attackers. Previous techniques for CFI may reduce the robustness of embedded and safety-critical systems, as they handle CFI violations by stopping programs. In this work, we present PCFIRE, a preventative approach to CFI that prevents the root-causes of CFI violations to allow recovery, and enables programmers to specify robust recovery actions by providing CFI via source-code safety-checks. PCFIRE's CFI can be formally proved automatically, and supports realistic features of embedded software such as hardware and I/O access. We showcase PCFIRE by providing and automatically proving CFI for: benchmark programs, text utilities containing I/O, and embedded programs with sensor inputs and hardware outputs on the Raspberry Pi single-board computer.
FULL PAPER: pdf