“One Weird Trick…”: Galois Develops Fuzzing Tool for User-Friendly Cryptographic Verification
Galois today announced the development of a new fuzzing tool aimed at streamlining the cryptographic verification process in the Software Analysis Workbench (SAW), part of a wider effort focused on making formal verification tools more practical, speedy, and user-friendly.
SAW provides the ability to formally verify properties of code written in C, X86_64, Java, and Cryptol. SAT and SMT solvers automate much of this process, but the most complex proofs require careful work by skilled proof engineers. Previously, one of the most difficult and time-consuming tasks was proving equivalences between complex mathematical terms. A proof engineer must look at a logical formula (for example, spec_term_A == implementation_term_B) and find equivalent subterms that can be rewritten. By performing this task repeatedly, a large logical term can be reduced step-by-step to one that can be automatically verified. But the cost was very high—hundreds of hours of proof engineering effort!
That’s where the fuzzing tool changes the game. To tackle this problem, Galois Research Engineer Andrei Stefanescu used a heuristic approach. The key insight is simple: while it is difficult to show that two subterms are equal (this requires considering all possible inputs), it’s very easy to show that they are not equal (we just have to find one counter-example). The fuzzing tool randomly synthesizes inputs to the formula, and gradually knocks out ‘candidate’ subterms that cannot possibly be equal. Then once the set of remaining candidates is small enough, we can use the SMT solver to check these equivalences automatically.
This trick seems almost too good to be true, but it works! In one of our tests, a rewriting process that would previously have taken at least 100 hours of manual work was reduced to a one-line command, followed by two minutes of compute time. It’s not magic: the reason this trick works so well is that SAW proofs often generate the correct type of equivalence. But Andrei’s fuzzing tool shows the incredible power of a well-chosen heuristic applied to a restricted domain.
Making Formal Methods More Accessible
The new fuzzing tool is just one part of Galois’s larger efforts to make formal methods and formal verification tools more applicable, practical, and usable in real-world scenarios.
Other similar projects include work by Stefanescu and fellow research engineer Sourya Dey, using machine learning to automatically select and verify some of the most time-consuming operations in the verification process. Galois Research Engineer Bretton Chen has also been working on support for Foreign Function Interface (FFI) in Cryptol. This work allows a Cryptol function to be defined in C, thereby significantly increasing its runtime speed.
At Galois, our approach to formal verification does not focus on one all-powerful tool or framework. Rather, we are building better tools step-by-step, by progressively improving utility, decreasing complexity, and tackling pain-points. By doing this, we are moving ever closer towards fully automated formal verification that integrates smoothly into software engineering pipelines. Big picture: we’re making these crucial tools not only more accessible but also faster, more efficient, more affordable, and ultimately more effective.