Multi-Language and Multi-Prover Verification with SAWScript

Presented as part of the 2015 HCSS conference.

Abstract:

SAWScript is a domain-specific language for orchestrating software analysis tasks, including formal proofs, that may involve multiple programming languages and multiple formal analysis tools, as part of the Software Analysis Workbench (SAW). SAWScript allows users to build and manipulate formal models representing the full semantics of code under analysis, from a variety of languages, including LLVM, JVM, and Cryptol. These formal models are represented within a single intermediate language, and can then be combined, transformed, and emitted to external proof tools such as SAT/SMT solvers and interactive theorem provers.

Using SAWScript allows an automated and integrated proof process, replacing what would otherwise have been a tedious and error-prone effort of manually combining results from a collection of subsidiary proof attempts. SAWScript is an integrated, interactive environment. It is not restricted to analyzing systems written in a single language, and one can compare, say C and Java implementations within the same SAWScript session. SAWScript also allows a variety of external solvers and proof tactics to be used within a single proof attempt. One could, for example, use one tool for reasoning about portions of the code involving arithmetic, and another for reasoning about bit-level semantics.

SAWScript has been used to verify equivalence of a number of production-quality algorithms, including implementations of Suite B cryptographic primitives from the OpenSSL and BouncyCastle libraries. This talk will demonstrate the use of SAWScript on a number of examples of verification and analysis.

Biography:

Dr. Aaron Tomb is an engineer and researcher at Galois, Inc., where he leads efforts in formal methods and software analysis. Dr. Tomb has a Ph.D. in Computer Science from the University of California, Santa Cruz. His research interests focus on techniques for improving the quality of software, including type systems, static analysis techniques, automated and interactive theorem provers, and the use of high-level and domain-specific programming languages. He has led a number of projects at Galois aimed at detecting software bugs or proving their absence, using techniques such as symbolic simulation, axiomatic verification, model checking, and automated code generation from verified models.