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 Ghosts of Departed Proofs
Date Thursday, February 02, 2023
Time 12:00 pm
Speaker Matt Noonan is a Principal Engineer at CrowdStrike.
Location Galois is pleased to host this tech talk via live-stream for the public on February 2, 2023 from 12:00 pm to 1:00 pm PDT. Send a request to firstname.lastname@example.org to receive meeting information.