International Association
for Cryptologic Research

Recent years have seen several landmark results in the formal verification of high-performance cryptographic libraries, leading to verified crypto code being adopted by mainstream projects like Chrome, Firefox, and Linux. Despite these successes, the secure integration and composition of verified cryptographic components within larger unverified applications remains an open challenge. The first problem is that each verification project uses its own formal specification language (F*, EasyCrypt, Coq), making its guarantees and assumptions hard for an application developer to read and understand. Second, each verified implementation presents its own low-level API that is easy to misuse. Third, when verified code is embedded within an application written in an unsafe language like C, any memory safety error in the surrounding unverified code may be used to attack the crypto code, potentially nullifying the formal guarantees of verification. In this talk, we propose a new approach that closes these gaps by integrating specification and verification within the cryptographic software development workflow. Our approach is built around HACSPEC, a new language for writing succinct, executable, formal specifications for cryptographic constructions, which aims to be equally accessible to developers, cryptographers, and verification experts. We describe translations from HACSPEC to F*, Coq, and EasyCrypt. We also present the first release of LIBCRUX, most comprehensive high- assurance cryptographic provider to date, combining verified code from HACL*, Fiat-Crypto, Vale, Jasmin, and AUCurves.