Axe

The Axe toolkit provides a variety of formal tools for program analysis and verification. It has been used to formally verify a variety of real-world Java bytecode and x86 binary programs, including cryptographic algorithms such as block ciphers and hash functions. Axe can perform symbolic execution to “lift” such programs into a logical representation. The Axe Equivalence Checker can then be applied to prove equivalence between the lifted implementation and a formal specification (or a second implementation). Axe can also prove properties of the lifted code and find inputs that trigger interesting program behaviors.

Axe is implemented on top of the ACL2 theorem prover and is based on the high-performance Axe Rewriter. Critically, the Axe Rewriter takes advantage of shared structure to represent mathematical terms not as operator trees but as DAGs (Directed Acyclic Graphs). This compact representation can prevent exponential explosion in the term size.

The Axe Rewriter applies ACL2 theorems as rewrite rules and performs symbolic execution using a formal model of the underlying machine. It currently works with models of the Java Virtual Machine and the x86 processor. Symbolic execution in Axe amounts to repeatedly stepping and simplifying a symbolic state, mimicking the effect of the program and accumulating a large symbolic result. This technique is standard in the ACL2 community, but a structure-shared term representation like the DAGs used by Axe is needed to make it scale. Axe can perform long symbolic executions (tens of thousands of instructions) and is quite performant (hundreds of thousands of rewrite rule attempts per second).

When lifting code, Axe deals with loops in two ways. When loop iteration counts are bounded, Axe can unroll the loops in the program, producing a large loop-free term representing the program’s effect on the machine state. When loops cannot be unrolled, the Axe Lifter can use loop invariants from the user (or from static analysis) to lift the loops into recursive functions in the ACL2 logic.

The result of lifting is an Axe DAG, which can then be subjected to a variety of analyses including property proving (via rewriting, bit-blasting, SMT queries, and other tactics) and SMT-based test input generation that can reveal interesting behaviors of the program. The Axe Equivalence Checker can be applied to prove equivalence of two lifted programs, or of a lifted program and a formal specification (often after using rewriting to unroll all recursions in the spec). It supports a variety of tactics, including rewriting, bit-blasting, SMT queries, and test-case-based identification of internal equivalences to break down the problem into smaller problems. Finally, a lifted program can be subjected to transformations from our APT toolkit to formally prove that it implements a given formal specification. That process works by refining the specification towards the lifted code and abstracting and un-refining the lifted code to make it more similar to the specification. Eventually, the two “meet in the middle”, yielding a chain of proven steps establishing how the program implements the specification.

The Axe Rewriter contains a variety of sophisticated features, including conditional rules, heuristic control of rule application, heuristic binding of free variables in rules, rule monitoring, rule priorities, the use of assumptions, and the use of contextual information (approximated because a node may occur in an exponential number of contexts). Because rewrite rules are usually proved as ACL2 theorems, new rules can be added without compromising the soundness of the system. Axe can be more flexible and higher-assurance than symbolic execution systems that use fixed sets of hand-implemented simplifications.

An earlier version of Axe is described in Eric Smith’s Ph.D. dissertation and his defense slides.

An very early version of Axe is also described in this paper: Automatic Formal Verification of Block Cipher Implementations. Eric Smith and David Dill. FMCAD ‘08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, November, 2008.
and in these accompanying slides.

A recent slide deck that includes a discussion of Axe is available here.

A video that discusses Axe is available on YouTube.

Axe is available as open-source software in the ACL2 community books.

Some Axe proofs about Java/JVM code can be found here.

Some Axe proofs about x86 binary code can be found here.