FMitF: Track II: Automated Verification for Assembly Implementations of Cryptography Libraries

Mainstream libraries for cryptography, like OpenSSL and BoringSSL, contain several thousand lines of manually optimized assembly code for high performance. Bugs in these systems are unfortunately somewhat common. This project develops techniques and a tool, CASM-Verify, to automatically check the equivalence of highly optimized assembly implementations of cryptographic algorithms against unoptimized reference versions of these algorithms in order to ensure that bugs are not introduced during the optimization process. The project's novelty is in decomposing the equivalence checking problem into several small sub-problems using a combination of concrete and symbolic evaluation. The project aims to improve the assurance of widely used cryptography libraries with usable equivalence checking tools. The project also will educate graduate and undergraduate students and practitioners on various formal tools and techniques.

The software developed as part of this project takes a given a reference and an optimized implementation, and concretely execute the two implementations on randomly generated inputs and identifies likely equivalent variables. Subsequently, it uses symbolic verification using satisfiability modulo theory solvers to determine whether the identified variables are indeed equivalent. Further, it decomposes the original query into small sub-queries using a collection of optimizations for memory accesses. To enable the usage of these ideas by mainstream developers, this project explores the following directions: (1) support Qhasm and Jasmin languages for high-speed cryptography, (2) support reasoning about large integer arithmetic, and (3) verify constant-time properties of assembly implementations.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.