Strange Loop

From Testing to Proof using Symbolic Execution

Developing correct software is hard enough when basic functionality is the key concern but becomes even more difficult when security comes into play. An attacker need only discover one bug to compromise the security of a system.

Testing is the most widely practiced approach for ensuring quality but by its nature is able to cover only a limited number of cases. In situations where security is critical, exhaustive testing would be ideal but is largely infeasible.

Fortunately, automated reasoning tools such as SAT and SMT solvers make something equivalent to exhaustive testing tractable. These tools can automatically determine whether certain mathematical propositions are true, and can be applied to software through the technique of symbolic execution. This workshop will introduce you to these tools and show you how to use them to prove the correctness of software.

The examples we cover will be drawn primarily from cryptography in part because cryptographic code is difficult to get right, and also because most cryptographic algorithms are clearly specified, so the properties to test are well understood.

We will describe these concepts in the context of an open source tool called the Software Analysis Workbench (SAW) which implements symbolic execution for Java and C and integrates with SAT and SMT solvers. It also allows specification of the desired functionality of code using the Cryptol language, originally designed for the specification of cryptographic algorithms.

Aaron Tomb

Aaron Tomb

Galois, Inc.

Dr. Tomb received his B.S., M.S., and Ph.D. in computer science from the University of California, Santa Cruz. His research focuses on programming language theory, and particularly on the use of advanced programming language technology to improve software reliability. This involves type theory, automated reasoning, program analysis, and a bit of subjective exploration into what makes languages pleasant to use. At Galois, he leads projects focused on applied formal methods, with a particular emphasis on the verification of cryptographic software. As part of this effort, he leads the development of the Software Analysis Workbench (SAW).