Galois Finishes REVERSER Project, Resulting in Automation and Efficiency Gains in Verification Tools

For decades, Galois has used mathematically rigorous formal verification techniques to establish the correctness of systems where failures could have severe consequences, such as safety-critical applications in aerospace, medical devices, cryptographic algorithms, blockchain, and autonomous vehicles. The process offers the highest possible levels of assurance—a must for critical systems—but is very time and labor-intensive. 

This week, Galois announces the completion of the Repair Engineering for Verified Software Resilience (REVERSER) project (a part of the DARPA Proof Engineering, Adaptation, Repair, and Learning for Software [PEARLS] AI Exploration), which makes formal verification for cryptography faster, less expensive, and more automated than ever before. Substantial upgrades to Galois’s Software Analysis Workbench (SAW) automate and simplify the most time-consuming and arduous parts of formal verification for cryptographic applications. 

Formally verifying a system typically requires deep expertise in building a correct proof and can be very time-consuming. In SAW, this step-by-step process involves applying different logical operations that move the system closer to verification. Now, the “AutoSAW” tool, developed as part of REVERSER, uses machine learning to automatically select and verify these operations, reducing the overall time required of human engineers and lowering the barrier for verifying a system. Galois has successfully demonstrated this functionality on proofs of AWS LibCrypto and blst, some of the most difficult existing proofs of cryptographic correctness and blockchain protocols. 

Simultaneously, Galois researchers on the REVERSER project have developed a functionality that enables SAW to automatically identify and verify looping variants—another task normally performed manually by engineers. In short, the advances achieved in the REVERSER project effectively automate and simplify the most time-consuming and arduous parts of formal verification for cryptographic applications. 

 A New Era for High Assurance Systems 

These innovations represent a significant step forward in automating formal verification. Machine learning can now solve more than 90% of new, unseen proofs. Importantly, the effectiveness of formal verification is not compromised; rather, it is made faster and more affordable with automated methods. 

While these upgrades are still under development, the results are already very promising: AutoSAW’s automated process has thus far worked on 94% of proofs tested. The tool is in the process of being open-sourced, and its results are planned to be submitted to the OOPSLA conference. 

It is worth noting that, while AutoSAW and the new looping variant verification functionality do streamline the process, they do not completely eliminate the need for human expertise. A human engineer is still needed to write the initial proof and build the groundwork for the machine learning tool to train on prior to its deployment. 

REVERSER’s SAW upgrades empower human experts by freeing them from repetitive and time-consuming tasks, allowing them to focus on complex, unique scenarios that require a higher level of human judgment. This blend of human expertise and groundbreaking technology provides Galois a unique advantage in creating a cheaper and more efficient formal verification process, inching us ever closer to a new era of high assurance for critical systems. 

Learn more about REVERSER HERE