AUSPICE-R

AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine-Code

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.

Test Programs

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:

  1. cat: Simple implementation of the cat text utility for printing a text file.
  2. wc: Simple implementation of the wc text utility for counting words in a text file.
  3. grep: Simple implementation of the grep text utility for searching for strings in a text file (only supports simple strings, no regular expressions supported).
  4. rpi_blink: Raspberry Pi hardware demonstration: Blink an LED a fixed number of times.
  5. rpi_light: Raspberry Pi hardware demonstration: Read an input from an analog light sensor, and turn on an LED if it is dark.
  6. rpi_lcd: Raspberry Pi hardware demonstration: Print a string to an 16x2 4-bit monochrome LCD.
  7. rpi_fall-det: Raspberry Pi fall detector: Reads data from an accelerometer to determine if the accelerometer has been dropped from a height; designed to detect falls in humans.
  8. arrcpy: Copies one array of integers to another.
  9. sort: Implementation of the Insertion Sort algorithm for integers.
  10. string_search: Implementation of the Boyer-Moore string search algorithm; part of the MiBench benchmark suite for embedded systems.

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.

Distribution

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.

Usage and License

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).