Typical software test methodology consists of throwing small samples of inputs at programs, either manually or though automated means. The assurance of these approaches is only as good as the sampling is representative of real world inputs. Savvy software and test engineers understand that these methods, when automated at all, provide only limited test coverage of the code. Unlike other types of engineering in the physical world, typical software programs do not implement continuous functions, so including even extensive sets of input samples into test processes provides no guarantee that all flaws are found.
While some software programs can (and are) mechanically generated by tools like Cryptol, software engineers looking for higher levels of assurance on existing, legacy or hand-generated code bases have had few tools to assist them. They are left with laborious testing and/or extant risk.
Our Solution: SAW
The Software Analysis Workbench (SAW) is a tool suite that can formally verify properties of code. It leverages mathematical solvers to make this process as automated as possible, and provides a scripting language called SAW Script that scales up verification to complex systems.
As a verification tool, SAW provides a level of assurance beyond the capabilities of traditional approaches. SAW can prove that a program works on all inputs, not just the inputs it was tested on, and is capable of finding counterexamples when program code doesn’t agree with its specification. Originally designed 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.
- Verification engineers can use SAW to prove that a program implements its specification.
- Security analysts can use SAW to generate models identifying constraints on program control flow, and to identify inputs that can reach potentially dangerous parts of a program.
- Cryptographers can use SAW to generate models from production cryptographic code for import and use within Cryptol.
While SAW was originally designed to work on cryptographic implementations, it can reason about many other classes of programs at the bit-level.
How it Works
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 implementations. Using these techniques, SAW is able to verify that code conforms to its specifications, and can compare different implementations for functional equivalence – enabling hand-coded optimizations to be verified as correct.
SAW supports analysis of programs written in C (via LLVM), Java™ (via JVM), MATLAB®, and Cryptol, and uses SAT and SMT solvers such as ABC, Yices, and Z3. SAW is able to use external solvers as well, extending its power further. SAW can be used to analyze entire programs, or can be applied to subsets of functions and their callees. SAW supports a variety of use cases including batch and interactive modes for closer inspection and experimentation.
We Admit it, This is Hard
Even with the SAW tool suite, applying formal verification to existing software for high-assurance systems is not something most software engineers are familiar with. That’s where Formaltech comes in. We can:
- Train your team on using SAW
- Assist you in the development, optimization and formal verification of your algorithms
- Verify your code for you