1<!-- 2 Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 4 SPDX-License-Identifier: CC-BY-SA-4.0 5--> 6 7The NICTA Graph Refinement Toolset 8================================== 9 10This is a set of tools which discover and check refinement proofs between 11programs with fairly arbitrary control flow graphs, including a number of 12kinds of loop relationships. The tools are written in python and make heavy 13use of SMT solvers. 14 15The design and theory of this tool are described in the paper [Translation 16Validation for a Verified OS Kernel][1] by Sewell, Myreen & Klein. 17 18 [1]: https://ssrg.nicta.com.au/publications/nictaabstracts/Sewell_MK_13.abstract.pml "Translation Validation for a Verified OS Kernel" 19 20Repository Setup 21---------------- 22 23This tool can be used as it is. It is also designed to link with the 24[L4.verified][2] proof chain. The full proof chain can be fetched via a 25Google [repo][3] setup. To obtain the full environment, instead of cloning 26this repository, follow the instructions in the [manifest repository][4] here: 27 28 https://github.com/seL4/verification-manifest 29 30To set up the various tools in the verification bundle, see the section 31[Dependencies](#dependencies) below. 32 33 [2]: https://github.com/seL4/l4v "L4.verified Repository" 34 [3]: http://source.android.com/source/downloading.html#installing-repo "google repo installation" 35 [4]: https://github.com/seL4/verification-manifest "Verification Manifest Repository" 36 37Examples 38-------- 39 40The [`example`](example/) and [`loop-example`](loop-example/) directories 41contain prebuilt example refinement targets. The [`example`](example/) 42directory contains a number of handwritten demonstration problems. The 43[`loop-example`](loop-example/) contains example compilation and decompilation 44of a simple example program involving a loop both the `-O1` and `-O2` arguments 45to `gcc`. Both versions should be provable, but the `-O2` version involves a 46loop unrolling that is computationally expensive to verify. 47 48The examples can be used to exercise the tool as follows: 49 50 python graph-refine.py example f g rotate_right has_value 51 python graph-refine.py loop-example/O1 all 52 53 # *much* slower 54 python graph-refine.py loop-example/O2 all 55 56The [`seL4-example`](seL4-example/) directory contains a recipe for building 57the seL4 binary verification problem. If this repository is set up via the 58[verification manifest][4] then most of the necessary components will be 59present. More information on running the full process is included in the 60[`seL4-example`](seL4-example/) directory. 61 62Dependencies 63------------ 64 65The tool requires the use of an SMT solver supporting the QF\_ABV logic, which 66is not provided here. Available solvers should be listed in a `.solverlist` 67configuration file. Further documentation will be given on the command line if 68the configuration is missing or invalide. The `.solverlist` file format is also 69documented in in [`solver.py`](solver.py). 70 71To test the solver setup is working: 72 73 python solver.py test 74 75Additional dependencies are required to run the full seL4 binary verification 76problem. They are described in the [`seL4-example`](seL4-example/) directory. 77 78Usage 79----- 80 81The tool is invoked by: 82 83 python graph-refine.py <target> <instructions> 84 85A target is a directory which contains all of the functions and configuration 86associated with an input problem. Target directories must contain a target.py 87setup script. See the example directory for an example. 88 89There are various instructions available: 90 91 - all: test all functions. this will usually be the last instruction. 92 - no-loops: skip functions with loops 93 - only-loops: skip functions without loops 94 - verbose: produce a lot of diagnostic output in subsequent instructions. 95 - `function-name`: other instructions will be taken as the name of a single 96function to be tested. 97 98Overview 99-------- 100 101 - [syntax.py](syntax.py): defines the syntax of the graph language and its parser. A syntax reference is included. 102 - [logic.py](logic.py): defines the top-level per-function proof obligations. Also provides various graph algorithms. 103 - [problem.py](problem.py): stores the state of one refinement problem. Keeps mutable copies of graph functions, allowing inlining. 104 - [solver.py](solver.py): controls the SMT solver. Manages an SMT problem state and some logical extensions. 105 - [rep\_graph.py](rep_graph.py): populates the solver state with a model produced from a problem. 106 - [check.py](check.py): defines the refinement proof format and the process for checking a proof. 107 - [search.py](search.py): searches for a refinement proof. 108 - [stack\_logic.py](stack_logic.py): provides additional analysis to address stack aspects of the binary calling convention. 109 - [graph-refine.py](graph-refine.py): top level. 110 111 - [trace\_refute.py](trace_refute.py): adaptation of this tool to detect 112 impossible traces. This may be useful for other static analysis, e.g. WCET 113 estimation. 114 - [debug.py](debug.py): debug helper code. 115 116 - [example](example), [loop-example](loop-example), 117 [seL4-example](seL4-example) are discussed in the [Examples](#examples) 118above. 119 120