Axe: An Automated Formal Equivalence Checking Tool for Programs

Presented as part of the 2012 HCSS conference.

Abstract:

This talk describes Axe, an automated formal verification tool for proving equivalence of programs. Axe has been used to verify real-world Java implementations of cryptographic operations, including block ciphers, stream ciphers, and cryptographic has functions. Axe proves the bit-for-bit equivalence of the outputs of two programs, one of which may be a formal, mathematical specification. To do so, Axe relies on a novel combination of techniques from combinational equivalence checking and inductive theorem proving. First, the loops in some programs can be completely unrolled, creating large loop-free terms. Axe proves the equivalence of such terms using a phased approach, including aggressive word-level simplifications, bit-blasting, test-case-cased identification of internal equivalences, and “sweeping and merging.” For loops that cannot be unrolled, Axe uses execution traces to detect loop properties, including loop invariants for single loops and connection relationships between corresponding loops. Axe proves such properties inductively. In many cases, synchronizing transformations must be performed to align the loop structures of the programs being compared; Axe can perform and verify a variety of these transformations.

Axe was the subject of the presenter’s Ph.D. dissertation at Stanford University (completed June, 2011).

Biography:

Eric W. Smith is a Computer Scientist at Kestrel Institute.  He has over a decade of experience with formal methods, especially theorem provers.  At Kestrel, he is involved in several projects, including leading Kestrel's effort to formally prove that Android applications comply with their security policies. He is also using Kestrel's Specware system to formally specify a virtual Trusted Platform Module (vTPM), with the goal of generating correct by-construction C code, including machine-checkable proofs of correctness in the Isabelle/HOL theorem prover.  Dr. Smith is also helping to design the security architecture of a multi-level secure fractionated satellite system.  Before joining Kestrel, Dr. Smith completed his Ph.D. in Computer Science at Stanford University under Professor David Dill.  His dissertation work included developing Axe, a theorem prover and equivalence checker capable of highly automated proofs of the correct operation of real-world cryptographic programs written in Java.  Axe was built on top of the ACL2 theorem prover, with which Dr. Smith has extensive experience.  He has used ACL2 for microprocessor verification at AMD and for processor modeling and machine code proofs at Rockwell Collins.  Dr. Smith did his undergraduate work at the University of Texas at Austin, where he earned bachelor's degrees in Computer Science and Plan II Honors under thesis advisor J. Moore.