We are pleased to announce a public preview of the Software Analysis Workbench.
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.
SAW has been particularly tuned toward the problem of equivalence checking: proving that two implementations of an algorithm, potentially written in different programming languages, have the same functional behavior for all possible inputs. 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), proving that the implementations are functionally equivalent to specifications written in Cryptol. We have used this to verify selected portions of existing, widely used libraries such as libgcrypt and BouncyCastle. Additional details on the project, including a tutorial, are available on the main project web site.
The SAW Script interpreter, the primary user interface to SAW, is freely available for non-commercial use. Several of the supporting libraries, including the implementation of the shared intermediate language SAW uses for representing models of software semantics, are available under a standard, 3-clause BSD license. If you have an interest in using SAW in a commercial context, contact us for a license tailored to your needs.
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 if you have any questions about SAW or high assurance development in general, and feel free to file issues on GitHub if you encounter problems.