This two part tutorial is an introduction to using SAW, the Software Analysis Workbench, to prove properties about imperative programs written in C. SAW uses symbolic execution to extract functional models from imperative programs, and SMT and SAT solvers to reduce the need for manual reasoning. It has been used to verify implementations of a number of cryptographic primitives.

The tutorial is divided into two sections:

• the first half focuses on learning to write specifications in Cryptol.
• the second half focuses on using SAW itself to reason about C programs.

These sections can be attended independently.

Cryptol is a purely-functional domain specific language for writing executable formal specifications. It has been used to specify a multitude of cryptographic algorithms and is the main language for writing functional behavior specifications in SAW.

The first half of the tutorial is an introduction to the Cryptol language. Our aim is to provide a basic understanding of the role and structure of the language, as well as some experience of writing Cryptol programs and using the Cryptol interpreter to evaluate, test, and verify the specifications. The second half of the tutorial is an example-driven introduction to SAW itself, and using SAW to verify C programs. Both halves of the tutorial will be fairly interactive, with relatively few slides, emphasizing practical experience with Cryptol and SAW.

To prepare for the first half, you should install the Cryptol interpreter, and download a copy of the “Programming Cryptol” book. For the second half, you should install SAW.