Binary Assurance Through Proofs Of Properties

Kestrel Technology is extending its Axe toolkit to build a lightweight, easy-to-use tool that can prove important safety, security, and correctness properties of software binaries, such as those used in off-the-shelf embedded systems. The tool combines the strengths of several of our existing tools: our Axe Lifter, which can transform x86 binaries into a logical form for further analysis; our Axe Prover, which can prove properties of lifted programs using a variety of proof tactics; our Axe Equivalence Checker, which can compare lifted programs to specifications or to known-good programs; and Axe's connections to SMT solvers, which can quickly discharge complex proof goals. In Phase I, we developed a prototype tool that can prove non-trivial properties of 64-bit ELF and Mach-O binary programs.  The tool uses Kestrel's Axe Lifter to explore a program or subroutine using symbolic execution, obtaining a mathematical term that represents its behavior. Lifting is done using the Axe Rewriter together with a model of the x86 CPU.  The lifted form represents the operation of the program on arbitrary data.  Kestrel's Axe Prover can then be used to prove properties of the lifted program, such as the fact that it satisfies given requirements, or computes the same result as some other program. A variety of proof tactics are available, including rewriting with our extensive library of proven rules, case splitting, and calling the ACL2 prover or an external SMT solver. The prototype tool, called the Formal Unit Tester for Binaries, provides a convenient way for users without formal methods training to check desired properties of a program. Unlike traditional unit tests, each of which covers a single input, formal unit tests are proofs that can cover very large input spaces. The user writes small test harnesses in a traditional programming language, and the tool attempts to prove that the tests always pass. Because the tests take inputs, each proof covers many possible computations. Often, the tool can provide assurance that all behaviors (perhaps within some bound on the input size) satisfy the desired property, or produce an input that violates the desired property. Our goal in Phase II will be to improve the usability, generality, and scalability of the tool and work to transition it to handle industrial use cases.