SAW (Software Analysis Workbench)
SAW provides analysts with the ability to extract formal models from programs, and analyze them using a variety of automated reasoning tools.
SAW supports analysis of programs written in C, Java, and Cryptol , and uses efficient SAT and SMT solvers such as ABC and Yices .
SAW is primarily designed with cryptographic implementations in mind, but also supports general purpose imperative programs.
Verification engineers can use SAW to prove that a program implements its specification.
Security analysts can have SAW generate models identifying constraints on program control flow to identify inputs that can reach potentially dangerous parts of a program.
Cryptographers can have SAW generate models from production cryptographic code for import and use within Cryptol.
The core of the SAW implementation, supporting C, Java, and Cryptol, is freely available under the standard 3-clause BSD license. See the main SAW website for or GitHub project for more details.
Most Recent Tech Talk
Title Public Tech Talk: “Stealthy Attacks and Attack-Resilient Interval Estimators”
Date Tuesday, July 20, 2021
Time 1:00 pm
Speaker Kwassi Degue is a Postdoctoral Associate in the Department of Aeronautics and Astronautics (AeroAstro) at Massachusetts Institute of Technology (MIT).
Location Galois was pleased to host this tech talk via live-stream for the public. A video of the presentation can be found below.