Vérification formelle de logiciels de sécurité à haute assurance en FStar: Application aux protocoles de communication et aux primitives cryptographiques
Benjamin Beurdouche · HAL (Le Centre pour la Communication Scientifique Directe) · 2020
The security of the modern Internet relies on cryptographic protocols such as TLS or Signal. However, the design and implementations of these protocols can have serious bugs which break their expected security guarantees. In this thesis, we will describe a novel class of statemachine attacks on TLS implementations which was hidden for years. The discovery of these attacks resulted in updates to all major web browsers and TLS implementations, but there are many other vulnerabilities which remain to be discovered. The central question we ask in this thesis is whether it is possible to design and implement cryptographic protocols in a way that is provably secure. Following a long line prior work, we advocate the use of formal verification to build high-assurance cryptographic software that systematically prevents such attacks. Existing methodologies include the analysis of high-level protocol models and verification of their reference implementations. However, there is a significant gap between existing verified code and efficient implementations. In this work, we propose to close this gap by developing verified cryptographic software in F* and compiling it to C. We develop reusable verified libraries that can be used by any project to build cryptographic software. We present HACL*, the first formally verified library providing a large panel of modern and performant cryptographic primitives in C. HACL* provides implementations of primitives that are proven memory-safe, functionally correct with respect to a formal specification, and offer protection against timing side-channels. We leverage our experience with HACL* to design LibSignal*, a verified implementation of Signal in WebAssembly. We relate LibSignal* to a model written in ProVerif through a weak syntacticargument in order to show that our implementation inherits security from the symbolic proof. Finally, we present the first formally verified specification and security proof in the Dolev-Yao model of TreeKEM, a new Tree-based Group Key Agreement used as part of the Messaging Layer Security (MLS) protocol at the IETF. HACL* is currently used within Mozilla Firefox,at Microsoft and in many other products, and our work on MLS has been instrumental in the IETF documents which we are co-authoring.