Read Intro to Verification and SAW Read Full Manual Development Roadmap
The Software Analysis Workbench (SAW) provides the ability to formally verify properties of code written in C, Java, and Cryptol. 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.
As a verification tool, SAW provides a level of assurance beyond the capabilities of traditional frameworks. 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.
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.
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.
SAW is closely connected with Cryptol, a domain-specific language Galois has 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.
SAW is available in source and binary form under the 3-clause BSD license.
An overview of using SAW can be found here. An academic paper describing it appeared in VSTTE’16.
You can see future development plans for SAW and other Galois tools here.
SAW is in active development, and we are currently making Alpha-quality Preview Releases available publicly. At Galois, we are passionate about improving the security and safety of critical software, and we think that verification tools such as SAW have an important role in achieving that goal.
We would love feedback on how to make SAW better. Please contact us at saw@galois.com if you have any questions about SAW or high assurance development in general. If you encounter any issues using SAW, please file a ticket on GitHub.