AutoCorres: automatic specification abstraction
AutoCorres is a program verification tool developed at
the Trustworthy Systems Group.
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.
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