Congratulations to Prof. Santosh Nagarakatte, who has just received an NSF grant for his project titled "FMitF: TrackII : Automated Verification for Assembly Implementations of Cryptography Libraries", for an amount of $99,996, for the period 08/01/2019-01/31/2021. He is the sole investigator on the project.
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 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. The project's novely 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 will also educate graduate and undergraduate students on formal methods for mainstream systems.
More details can be found on National Science Foundation's webpage: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1917897
Department of Computer Science