AutoCorres: automatic specification abstraction

AutoCorres is a program verification tool developed at the Trustworthy Systems Group.

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

Downloads

AutoCorres requires Isabelle 2020. The downloads below include a bundled copy of the C-to-Isabelle parser, which is also required for AutoCorres. The tool is released under a BSD-style license, however some bundled components are under other licenses. Please refer to copyright notices included in the release for further details.

Not using Isabelle2020? See our older releases.

Current release and documentation

Download AutoCorres 1.7 (Released 2020-11-02, Isabelle 2020)

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

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

Changelog

AutoCorres 1.7

• Isabelle2020 edition of both AutoCorres and the C parser.
• Slight updates to wp: use "wp (once)" instead of "wp_once".

AutoCorres 1.6.1

• Correct license for a C parser file. No code changes.

AutoCorres 1.6

• Isabelle2019 edition of both AutoCorres and the C parser.
• Word abstraction has been extended to C bitwise operators.

AutoCorres 1.5

• Isabelle2018 edition of both AutoCorres and the C parser.

AutoCorres 1.4

• Isabelle2017 edition of both AutoCorres and the C parser.

AutoCorres 1.3

• Isabelle2016-1 edition of both AutoCorres and the C parser.
• AutoCorres and the C parser now support multiple architectures, and require the L4V_ARCH environment variable to be set according to your choice of architecture. See the README for details.

AutoCorres 1.2

• Isabelle2016 edition of both AutoCorres and the C parser.
• Incompatibility: functions excluded using the “scope” option are no longer translated to “fail”. Instead, they are translated to a wrapper around the C parser's specs. This makes it possible to do proofs on “scope”-limited AutoCorres specs.

AutoCorres 1.1

• Isabelle2015 edition of both AutoCorres and the C parser.
• New options for changing how AutoCorres names functions and globals.
• Incompatibility: names of global variables have changed. Names have changed from “lifted_globals.foo_'” to “lifted_globals.foo_''”. Recover the old behaviour by setting lifted_globals_field_suffix="_'".
• Minor incompatibility: intermediate function names have changed. They are now “l1_foo'”, “l2_foo'”... instead of “l1_foo”, “l2_foo”.
• Renamed “ccorres” predicate to “ac_corres” for clarity.

Development

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

Old releases

• AutoCorres 1.6.1 (Released 2019-10-03, Isabelle 2019)
• AutoCorres 1.6 (Released 2019-09-05, Isabelle 2019)
• AutoCorres 1.5 (Released 2018-09-05, Isabelle 2018)
• AutoCorres 1.4 (Released 2018-03-02, Isabelle 2017)
• AutoCorres 1.3 (Released 2017-04-03, Isabelle 2016-1)
• AutoCorres 1.2 (Released 2016-03-31, Isabelle 2016)
• AutoCorres 1.1 (Released 2015-10-09, Isabelle 2015)
• AutoCorres 1.0 (Released 2014-12-16, Isabelle 2014)
• AutoCorres 0.999 (Released 2014-10-15, Isabelle 2014)
• AutoCorres 0.98 (Released 2014-06-26, Isabelle 2013-2)
• AutoCorres 0.97 (Released 2014-06-05, Isabelle 2013-2)
• AutoCorres 0.95-beta3 (Released 2014-02-11, Isabelle 2013-2)
• AutoCorres 0.95-beta2 (Released 2014-02-06, Isabelle 2013-2)
• AutoCorres 0.95-beta1 (Released 2014-01-17, Isabelle 2013-2)
• AutoCorres 0.9-beta3 (Released 2013-09-26, Isabelle 2013)
• AutoCorres 0.9-beta2 (Released 2013-09-22, Isabelle 2013)
• AutoCorres 0.9-beta1 (Released 2013-08-28, Isabelle 2013)
• AutoCorres 0.1 (Released 2012-12-05, Isabelle 2012)
• AutoCorres 0.0 (Released 2012-08-15, Isabelle 2011-1)

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