Skip to main content

AutoCorres : Automatic Specification Abstraction

AutoCorres : Automatic Specification Abstraction

AutoCorres is a research project of the Trustworthy Systems Group.

Spec chain
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: Before source code can be formally reasoned about, it must first be translated into the logic of a theorem prover. For example, to prove properties about C source code using the Isabelle/HOL theorem prover, a tool would be required to first convert the C into Isabelle/HOL, such as NICTA's C-to-Isabelle parser.

    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.

    This project aims to automatically abstract 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. Because the developed tool will generate a proof of correspondence between the generated high-level specification and the input low-level specification, 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 2016-1. 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.

Current Release and Documentation

Download AutoCorres 1.3 (Released 2017-04-03, Isabelle 2016-1)

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

Development versions of AutoCorres are available as a git repository hosted on GitHub.

Old Releases

Publications

Abstract PDF David Greenaway
Automated proof-producing abstraction of c code
PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015
Abstract PDF 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
Abstract PDF 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

Past

Served by Apache on Linux on seL4.