REVERSER

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. 

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) makes formal verification for cryptography faster, less expensive, and more automated than ever before. 

At its core, REVERSER aims to make a substantial upgrade to Galois’s Software Analysis Workbench (SAW), which provides the ability to formally verify properties of code written in C, Java, and Cryptol. SAW has been successfully used in the past to verify numerous high-impact systems, including verifying Amazon Web Services (AWS) cryptographic libraries, which provide data security for millions across the globe. 

Despite its efficacy, verifying complex systems with SAW requires deep expertise in building a correct proof and can be extremely time-consuming. Normally, this involves human engineers spending many hundreds of hours manually selecting rewrites, unfoldings, and uninterpreted terms to move the system closer to verification. Now, the “AutoSAW” tool, developed as part of REVERSER, uses machine learning to automatically select and verify these elements, 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. 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. In other words, 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. 

Key Benefits:

• Reduce the painstaking manual effort involved in formal verification.
• Improve efficiency in the verification process via automation.
• Wide usability across a range of proof sets such as AWS libcrypto (AWS-LC) and Supranational/blst.
• Provide continuous assurance and proof repair, reducing the amount of manual work and time needed for formal verification.

Why Galois?

Our team has deep expertise in formal verification and machine learning, and a solid track record of delivering innovative solutions to complex problems. Our work on REVERSER has laid the groundwork for more efficient, automated formal verification, a significant step forward in the field. We are committed to further enhancements and making formal verification more comprehensive, efficient, and user-friendly. We believe our unique approach to solving these pressing challenges sets us apart and positions us to deliver more effective solutions in the future.