14th Asian Symposium on Programming Languages and Systems (APLAS), November 2016.
Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, Priya Narasimhan
Carnegie Mellon University
*Intel Labs
Automatically generating proofs of safety properties for soft- ware is important as software becomes safety-critical, e.g., in medical devices and automobiles. While current techniques can automatically prove safety properties for machine code, they either: (i) do not support user-mode programs in an operating system, (ii) do not support realistic program features such as system calls, or (iii) have been demonstrated only on programs of limited sizes. We present AUSPICE-R, which au- tomates safety-property proof generation for user-mode ARM machine code containing system calls, and greatly improves the scalability of auto- mated safety-property proof generation. AUSPICE-R uses an axiomatic approach to model system calls, and leverages idioms in compiled code to optimize its proof automation. We demonstrate AUSPICE-R on (i) sim- ple working versions of common text utilities that perform I/O, and (ii) embedded programs for the Raspberry Pi single-board-computer con- taining hardware I/O. AUSPICE-R automatically proves safety up to 12x faster, and supports programs 3x larger, than prior techniques.
FULL PAPER: pdf