Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, Priya Narasimhan
Carnegie Mellon University
Under submission to the 14th Asian Symposium on Programming Languages and Systems (APLAS) 2016
Automating proofs of safety properties for software is important as software becomes increasingly safety-critical, e.g., in medical devices and automobiles. It is desirable to provide such proofs automatically, without users needing in-depth knowledge of formal methods. While current techniques can automatically prove safety properties for machine-code, they either do not support user-mode programs running in an operating system, or do not support realistic program features e.g., system calls.
We present AUSPICE-R, which automates safety property proof generation for user-mode ARM machine-code containing system calls, and greatly improves the scalability of automated safety-property proof generation. AUSPICE-R uses an axiomatic approach to model syscalls, and leverages idioms in compiled code to optimize its proof automation.
We demonstrate AUSPICE-R on (i) simple but fully-functioning versions of common text utilities that perform I/O, and (ii) embedded programs for the Raspberry Pi single-board-computer containing hardware inputs and outputs. AUSPICE-R automatically proves safety up to 12x faster, and for programs 3x larger, than prior techniques.
We are making available the test programs used to evaluate AUSPICE-R. The following parts of our test programs are available:
There are a total of 10 test programs:
Our test programs can be downloaded here.
The safety proofs for each of our test programs can also be downloaded here. Each file contains the console output from HOL4 of the safety theorems for each function in each test program, as stored in an ML dict structure.
This code is currently released for research purposes only.
Parts of the code licensed under LGPLv3 (WiringPi derived code) can be modified and distributed freely, providing the terms of LGPLv3 are adhered to, and the relevant copyright notices are retained.
Parts of the code derived from MiBench (string_search) in the public domain are covered under GPL and can also be modified and distributed freely.
All other parts of the code (including but not restricted to the safety checks in system-common/safety.h) are for research purposes only and not currently for commercial use.
The AUSPICE-R Test Programs are distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Parts of the AUSPICE-R Test Programs are based on the following libraries/projects and have been modified to add safety-checks for AUSPICE and AUSPICE-R.
Usage of the WiringPi library (and our modified/derived safe versions of the Raspberry Pi GPIO access code) is covered by the GNU Lesser General Public License version 3 (license file included in the zip file above).