SAW: The Software Analysis Workbench
Last updated
Last updated
The Software Analysis Workbench (SAW) is a tool that provides the ability to formally verify properties of code written in C, Java, Rust, and . It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAWScript, to enable verification to scale up to more complex systems. We also provide a remote procedure call (RPC) API and offer a Python library that interfaces with the RPC API.
Comprehensive Assurance: As a formal verification tool, SAW is capable of showing that your program works on all inputs, not just the ones it was tested on, and is capable of finding counterexamples when code doesn’t agree with its specification.
Open Source Library: You can access the code for SAW in our open source repository.
Behind the scenes, SAW leverages symbolic execution to translate code into formal models. During this process it executes code on symbolic inputs, effectively unrolling loops, and translating the code into a circuit representation. Symbolic execution is well suited to verifying code with bounded loops such as cryptographic verification.
At Galois, we have used SAW primarily to verify implementations of cryptographic algorithms such as the AES block cipher, the Secure Hash Algorithm (SHA), and Elliptic Curve Digital Signature Algorithm (ECDSA). We have used this to verify existing widely used libraries such as libgcrypt and Bouncy Castle.
We also have used SAW in collaboration with Amazon to prove the correctness of the HMAC implementation in their s2n implementation of the TLS protocol. You can read more about that work here.
More broadly, Cryptol and SAW have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and data safe; secure financial transactions; and protect the privacy of millions of people across the globe. The high assurance approach they represent forms the backbone—both technologically and philosophically—of Galois’s larger effort to create trustworthiness in the most critical systems on the planet, and to maximize impact through sharing these powerful tools with the open source community.
The R&D community, industry, and the public at large can benefit when tools like SAW are open sourced. In addition, open-source tools can themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, Galois has developed SAW as an open source tool from the very beginning, and the tool is open for anyone to use and explore.
Scalable Security: and SAW automate much of the most time-consuming parts of formal verification, enabling the process to scale to complex systems.
SAW is closely connected with , a domain-specific language Galois created for the high-level specification of cryptographic algorithms. The most common use of SAW is to prove equivalence between a Cryptol specification of an algorithm and a production implementation written in a language such as C or Java.
