AutoCorres: automatic specification abstraction

AutoCorres is a program verification tool developed at Trustworthy Systems.

C code is automatically abstracted into increasingly more abstract specifications, easing manual reasoning about the code.

• Aim: Simplify formal verification of C code by automatically and provably abstracting low-level C semantics into higher-level representations.

• Overview: AutoCorres is an automatic abstraction tool that can be used in conjunction with our C-to-Isabelle parser.

  The C parser translates C code into the logic of the Isabelle/HOL theorem prover. A delicate choice must be made when designing such a translator. On one hand, it is desirable to make the translator as simple as possible: if the translator incorrectly imports source code into logic, than proofs carried out on the imported program may not apply to the actual source code. On the other hand, the translated source code will need to be later manually reasoned about: if the translator only provides a primitive translation of source code, later reasoning will be cumbersome and time-consuming.

  AutoCorres automatically abstracts low-level translated programs into a form better suited for human reasoning. This allows the translation from source code into logic to remain simple (allowing users to have confidence in the translation) while still allowing program verifiers to work with a higher-level specification of the source code. This tool generates a proof of correspondence between the generated high-level specification and the input low-level specification, so users can be confident in the results.

• Results:

  • AutoCorres can automatically and provably convert C programs into a higher-level monadic representation.
  • AutoCorres' heap abstraction feature allows users to carry out high-level reasoning about memory for type-safe functions, while still allowing byte-level reasoning where necessary.
  • AutoCorres' word abstraction feature can automatically and soundly abstract two's-complement machine words into unbounded natural numbers and integers, simplifying reasoning.
  • AutoCorres can be used to reason about non-trivial programs: it can parse the seL4 microkernel source code, for example.
  • AutoCorres allows high-level reasoning: an existing proof of the Schorr-Waite algorithm based on a highly-abstract machine could be ported to the output of AutoCorres on a concrete C implementation with minimal effort.
  • AutoCorres generates a proof of correctness in Isabelle/HOL for all of its translations. This means that you don't need to trust AutoCorres to soundly reason about its output.

AutoCorres (up to 1.0) was developed by David Greenaway. Most of its theories and algorithms are described in his PhD thesis.

Current release and documentation

See the AutoCorres GitHub relases for the latest version of AutoCorres and a bundled version of the C-to-Isabelle parser.

Quickstart Guide (PDF): A whirlwind introduction to AutoCorres.

The supplied README gives an overview of the available AutoCorres configuration options and example proofs.

Changelog

See the latest change log on GitHub.

Development

AutoCorres is developed as part of the L4.verified repository, in the tools/autocorres directory.

Publications

		David Greenaway Automated proof-producing abstraction of c code PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015
		David Greenaway, Japheth Lim, June Andronick and Gerwin Klein Don't sweat the small stuff: Formal verification of C code without the pain ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 429–439, Edinburgh, UK, June, 2014
		David Greenaway, June Andronick and Gerwin Klein Bridging the gap: Automatic verified abstraction of C International Conference on Interactive Theorem Proving, pp. 99–115, Princeton, New Jersey, USA, August, 2012

People