The Software Analysis Workbench (SAW) is one of Galois’s flagship verification tools. SAW has been used to verify important, real-world cryptographic algorithms, such as 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. SAW is highly automated, using a combination of symbolic execution, automated solvers, and human guidance. Traditionally, SAW proofs are orchestrated using SAWScript, a custom DSL reminiscent of ML and Haskell. Recently, however, my colleagues and I have been working on a new interface to SAW. This new interface is a JSON-RPC API that enables SAW to be controlled from any language. Or at least any language that supports either sockets or pipes!
As part of this ongoing development, we’ve constructed a Python interface. Using a popular programming language lowers the entry barriers for new users. It gives us access to a rich world of libraries, making it much easier to produce convenient user interfaces.
This video demonstrates our prototype Python interface to SAW. I hope you enjoy it!