Kestrel Technology proposes to extend 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. This will combine 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 our Formal Unit Tester, which helps users without formal methods expertise explore bounded program behaviors. The latter tool currently operates on Java programs but will be retargeted to binaries. We plan to target x86 but can pivot to a different CPU type if desired. Kestrel's Axe Lifter can 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 target machine (currently, the Java Virtual Machine or x86 CPU). The lifted form represents the operation of the program on arbitrary data. Axe has techniques to avoid path explosion (rejoining the execution after conditional branches) and can lift entire loops into recursive functions. Kestrel's Axe Prover can then be used to prove properties of the lifted program, such as the fact that program operation satisfies given requirements. 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. Kestrel's Axe Equivalence Checker can prove the equivalence of two lifted programs, or of a program and a specification. This provides a convenient way to specify correct behavior, and the proof can be highly automatic when the amount of computation is bounded (e.g., when loops can be unrolled). Kestrel's Formal Unit Tester, currently only for Java bytecode programs, 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 small 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 can take symbolic inputs, each covers many possible computations. The tool can provide assurance that all behaviors (perhaps within some bound on the input size) satisfy the desired property. Or it can produce an input that violates the desired property. The novelty of the project will be to combine all these tools, bringing the above capabilities to binaries. We will also improve the automation, usability, and scalability of the tools and apply them to industrial use cases.
