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 SAW Script, 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.
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 available in source and binary form under the 3-clause BSD license.
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 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.