This is a set of tools which discover and check refinement proofs between programs with fairly arbitrary control flow graphs, including a number of kinds of loop relationships. The tools are written in python and make heavy use of SMT solvers.
The design and theory of this tool are described in the paper Translation Validation for a Verified OS Kernel by Sewell, Myreen & Klein.
This tool can be used as it is. It is also designed to link with the L4.verified proof chain. The full proof chain can be fetched via a Google repo setup. To obtain the full environment, instead of cloning this repository, follow the instructions in the manifest repository here:
https://github.com/seL4/verification-manifest
To set up the various tools in the verification bundle, see the section Dependencies below.
The example and loop-example directories
contain prebuilt example refinement targets. The example
directory contains a number of handwritten demonstration problems. The
loop-example contains example compilation and decompilation
of a simple example program involving a loop both the -O1 and -O2 arguments
to gcc. Both versions should be provable, but the -O2 version involves a
loop unrolling that is computationally expensive to verify.
The examples can be used to exercise the tool as follows:
python graph-refine.py example f g rotate_right has_value
python graph-refine.py loop-example/O1 all
# *much* slower
python graph-refine.py loop-example/O2 all
The seL4-example directory contains a recipe for building
the seL4 binary verification problem. If this repository is set up via the
verification manifest then most of the necessary components will be
present. More information on running the full process is included in the
seL4-example directory.
The tool requires the use of an SMT solver supporting the QF_ABV logic, which
is not provided here. Available solvers should be listed in a .solverlist
configuration file. Further documentation will be given on the command line if
the configuration is missing or invalide. The .solverlist file format is also
documented in in solver.py.
To test the solver setup is working:
python solver.py test
Additional dependencies are required to run the full seL4 binary verification
problem. They are described in the seL4-example directory.
The tool is invoked by:
python graph-refine.py <target> <instructions>
A target is a directory which contains all of the functions and configuration associated with an input problem. Target directories must contain a target.py setup script. See the example directory for an example.
There are various instructions available:
- all: test all functions. this will usually be the last instruction.
- no-loops: skip functions with loops
- only-loops: skip functions without loops
- verbose: produce a lot of diagnostic output in subsequent instructions.
function-name: other instructions will be taken as the name of a single function to be tested.
-
syntax.py: defines the syntax of the graph language and its parser. A syntax reference is included.
-
logic.py: defines the top-level per-function proof obligations. Also provides various graph algorithms.
-
problem.py: stores the state of one refinement problem. Keeps mutable copies of graph functions, allowing inlining.
-
solver.py: controls the SMT solver. Manages an SMT problem state and some logical extensions.
-
rep_graph.py: populates the solver state with a model produced from a problem.
-
check.py: defines the refinement proof format and the process for checking a proof.
-
search.py: searches for a refinement proof.
-
stack_logic.py: provides additional analysis to address stack aspects of the binary calling convention.
-
graph-refine.py: top level.
-
trace_refute.py: adaptation of this tool to detect impossible traces. This may be useful for other static analysis, e.g. WCET estimation.
-
debug.py: debug helper code.
-
example, loop-example, seL4-example are discussed in the Examples above.