Journal Publications and Book Chapters
Computer-Aided Proofs in Cryptography: An overview, with Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt and Pierre-Yves Strub.
All about Proofs, Proofs for All. Vol 55. Mathematical Logic and Foundations. 2015.
A brief introduction to some of the recent developments in computer-aided cryptography, including CertiCrypt, EasyCrypt, ZooCrypt and more specialized tools.
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with Andrew D. Gordon, Jan Jürjens and David A. Naumann.
Journal of Computer Security. 22(5):823-866, 2014.
An extended version of the CSF paper, using the (then) new version of VCC and extending a bit on the Coq aspects of the verification.
EasyCrypt: A Tutorial, with Gilles Barthe, Benjamin Grégoire, César Kunz, Benedikt Schmidt and Pierre-Yves Strub.
Foundations of Security Analysis and Design VII. Vol. 8604. Lecture Notes in Computer Science. 2013.
A short EasyCrypt tutorial giving an intuition of how detailed cryptographic proofs can easily be expressed in EasyCrypt.
Refereed Conference Publications
Strong Non-Interference and Type-Directed Higher-Order Masking, with Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub and Rébecca Zucchini.
In 23rd ACM Conference on Computer and Communications Security (ACM CCS 2016), to appear.
Differential power analysis (DPA) is a side-channel attack in which an adversary retrieves cryptographic material by measuring and analyzing the power consumption of the device on which the cryptographic algorithm under attack executes. An effective countermeasure against DPA is to mask secrets by probabilistically encoding them over a set of shares, and to run masked algorithms that compute on these encodings. Masked algorithms are often expected to provide, at least, a certain level of probing security.
Leveraging the deep connections between probabilistic information flow and probing security, we develop a precise, scalable, and fully automated methodology to verify the probing security of masked algorithms, and generate them from unprotected descriptions of the algorithm. Our methodology relies on several contributions of independent interest, including a stronger notion of probing security that supports compositional reasoning, and a type system for enforcing an expressive class of probing policies. Finally, we validate our methodology on examples that go significantly beyond the state-of-the-art.
Verifying Constant-Time Implementations, with José Bacelar Almeida, Manuel Barbosa, Gilles Barthe and Michael Emmi.
In 25th USENIX Security Symposium (USENIX Security 2016), pages 53--70.
The constant-time programming discipline is an effective countermeasure against timing and cache-timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to it is hard, especially under additional efficienty and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software. We propose a novel approach, based on the construction of a selective product program, for verifying constant-time security of real-world code, including implementations that locally and intentionally violate strict constant-time when such violations are benign with respect to the desired security property. To illustrate the practicality of our approach, we implement our approach in a fully automated prototype, ct-verif, that leverages the Smack and Boogie tools and verifies constant-time properties of optimized LLVM code, thereby removing the main part of the compiler from the TCB for side-channel security. We present verification results obtained over a wide range of constant-time components, from cryptographic (NaCl, FourQLib, OpenSSL, ...) and non-cryptographic (libfixedtimefixedpoint, ...) off-the-shelf libraries.
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC, with José Bacelar Almeida, Manuel Barbosa and Gilles Barthe.
In 23rd International Conference on Fast Software Encryption (FSE 2016), pages 163--184. Best paper award.
We provide further evidence that implementing software countermeasures against timing attacks is a non-trivial task and requires domain-specific software development processes: we report an implementation bug in the S2N library, recently released by AWS Labs. This bug (now fixed) allowed bypassing the balancing countermeasures against timing attacks deployed in the implementation of the MAC-then-Encode-then-CBC-Encrypt (MEE-CBC) component, creating a timing side-channel similar to that exploited by Lucky 13. Although such an attack could only be launched when the MEE-CBC component is used in isolation - Albrecht and Paterson recently confirmed in independent work that S2N's second line of defence provides adequate mitigation - its existence shows that conventional software validation processes are not being effective in this domain. To solve this problem, we define a methodology for proving security of implementations in the presence of timing attackers: first, prove black-box security of an algorithmic description of a cryptographic construction; then, establish functional correctness of an implementation with respect to the algorithmic description; and finally, prove that the implementation is leakage secure. We present a proof-of-concept application of our methodology to MEE-CBC, bringing together three different formal verification tools to produce an assembly implementation of this construction that is verifiably secure against adversaries with access to some timing leakage. Our methodology subsumes previous work connecting provable security and side-channel analysis at the implementation level, and supports the verification of a much larger case study. Our case study itself provides the first provable security validation of complex timing countermeasures deployed, for example, in OpenSSL.
Verified Proofs of Higher-Order Masking, with Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire and Pierre-Yves Strub.
In Advances in Cryptology -- EUROCRYPT 2015 -- 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, pages 457--485.
In this paper, we study the problem of automatically verifying higher-order masking countermeasures. This problem is important in practice (weaknesses have been discovered in schemes that were thought secure), but is inherently exponential: for t-order masking, it involves proving that every subset of t intermediate variables is distributed independently of the secrets. Some type systems have been proposed to help cryptographers check their proofs, but many of these approaches are insufficient for higher-order implementations. We propose a new method, based on program verification techniques, to check the independence of sets of intermediate variables from some secrets. Our new language-based characterization of the problem also allows us to design and implement several algorithms that greatly reduce the number of sets of variables that need to be considered to prove this independence property on all valid adversary observations. The result of these algorithms is either a proof of security or a set of observations on which the independence property cannot be proved. We focus on AES implementations to check the validity of our algorithms. We also confirm the tool's ability to give useful information when proofs fail, by rediscovering existing attacks and discovering new ones.
Synthesis of Fault Attacks on Cryptographic Implementations, with Gilles Barthe, Pierre-Alain Fouque, Benjamin Grégoire and Jean-Christophe Zapalowicz.
In Proceedings of the 2014 ACM SIGSAC conference on Computer & Communications Security (CCS 2014), pages 1016--1027.
Fault attacks are active attacks in which an adversary with physical access to a cryptographic device, for instance a smartcard, tampers with the execution of an algorithm to retrieve secret material. Since the seminal Bellcore attack on RSA signatures, there has been extensive work to discover new fault attacks against cryptographic schemes, and to develop countermeasures against such attacks. Originally focused on high-level algorithmic descriptions, these works increasingly focus on concrete implementations. While lowering the abstraction level leads to new fault attacks, it also makes their discovery significantly more challenging. In order to face this trend, it is therefore desirable to develop principled, tool-supported approaches that allow a systematic analysis of the security of cryptographic implementations against fault attacks. We propose, implement, and evaluate a new approach for finding fault attacks against cryptographic implementations. Our approach is based on identifying implementation-independent mathematical properties we call fault conditions. We choose them so that it is possible to recover secret data purely by computing on sufficiently many data points that satisfy a fault condition. Fault conditions capture the essence of a large number of attacks from the literature, including lattice-based attacks on RSA. Moreover, they provide a basis for discovering automatically new attacks: using fault conditions, we specify the problem of finding faulted implementations as a program synthesis problem. Using a specialized form of program synthesis, we discover multiple faulted implementations on RSA and ECDSA that realize the fault conditions, and hence lead to fault attacks. Several of the attacks found by our tool are new, and of independent interest.
Making RSA-PSS Secure Against Random Faults, with Gilles Barthe, Benjamin Grégoire, Pierre-Alain Fouque, Mehdi Tibouchi and Jean-Christophe Zapalowicz.
In Proceedings of the 2014 Workshop on Cryptographic Hardware and Embedded Systems (CHES 2014), pages 206--222.
RSA–CRT is the most widely used implementation for RSA signatures. However, deterministic and many probabilistic RSA signatures based on CRT are vulnerable to fault attacks. Nevertheless, Coron and Mandal (Asiacrypt 2009) show that the randomized PSS padding protects RSA signatures against random faults. In contrast, Fouque et al. (CHES 2012) show that PSS padding does not protect against certain non-random faults that can be injected in widely used implementations based on the Montgomery modular multiplication. In this article, we prove the security of an infective countermeasure against a large class of non-random faults; the proof extends Coron and Mandal’s result to a strong model where the adversary can force the faulty signatures to be a multiple of one of the prime factors of the RSA modulus. Such non-random faults induce more complex probability distributions than in the original proof, which we analyze using careful estimates of exponential sums attached to suitable rational functions. The security proof is formally verified using appropriate extensions of EasyCrypt, and provides the first application of formal verification to provable (i.e. reductionist) security in the context of fault attacks.
Certified Computer-Aided Cryptography: Efficient Provably Secure Machine Code from High-Level Implementations, with J. C. Bacelar Almeida, Manuel Barbosa and Gilles Barthe.
In Proceedings of the 2013 ACM SIGSAC conference on Computer & Communications Security (CCS 2013), pages 1217--1230.
We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealised probabilistic operations in the style of code-based security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries providing complex arithmetic calculations or instantiating idealised components such as sampling operations. This certified compiler allows us to carry to executable code the security guarantees established at the high-level, and is also instrumented to detect when compilation may interfere with side-channel countermeasures deployed in source code. We demonstrate the applicability of the framework with the RSA-OAEP encryption scheme, as standardized in PKCS#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of assembly implementations of the algorithms specified by the standard. The example also provides two contributions of independent interest: it is the first application of computer-aided cryptographic tools to real-world security, and the first application of CompCert to cryptographic software.
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with Andrew D. Gordon, Jan Jürjens and David A. Naumann.
In Proceedings of the 24th IEEE Symposium on Computer Security Foundations (CSF 2011), pages 3--17.
We describe how to verify security properties of C code for cryptographic protocols by using a general-purpose verifier. We prove security theorems in the symbolic model of cryptography. Our techniques include: use of ghost state to attach formal algebraic terms to concrete byte arrays and to detect collisions when two distinct terms map to the same byte array; decoration of a crypto API with contracts based on symbolic terms; and expression of the attacker model in terms of C programs. We rely on the general-purpose verifier VCC; we guide VCC to prove security simply by writing suitable header files and annotations in implementation files, rather than by changing VCC itself. We formalize the symbolic model in Coq in order to justify the addition of axioms to VCC.
- Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler, with Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire and Pierre-Yves Strub.
- Verified Implementations for Secure and Verifiable Computation, with José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, Benjamin Grégoire and Pierre-Yves Strub.
- Proving Computational Security with a General-Purpose C Verifier, with Cédric Fournet and Andrew D. Gordon. FCC 2012 and ASA-6, Harvard University, June 2012.
Verifying Cryptographic Code in C: Some Experience and the Csec Challenge, with Mihhail Aizatulin, Andrew D. Gordon and Jan Jürjens.
In Proceedings of the 8th International Workshop on Formal Aspects of Security and Trust (FAST'11), Leuven, September 2011. LNCS 7140. Invited paper.
The security of much critical infrastructure depends in part on cryptographic software coded in C, and yet vulnerabilities continue to be discovered in such software. We describe recent progress on checking the security of C code implementing cryptographic software. In particular, we describe projects that combine verification-condition generation and symbolic execution techniques for C, with methods for stating and verifying security properties of abstract models of cryptographic protocols. We illustrate these techniques on C code for a simple two-message protocol.
Verifying Authentication Properties of C Security Protocol Code Using General-Purpose Verifiers, with Andrew D. Gordon and Jan Jürjens.
ASA-4, FLoC, Edinburgh, July 2010.
We describe how a general purpose C verifier can be used to verify authentication properties of protocol implementations in a way similar to that of F7. We also give an informal security model, based on an assumed translation of verified C programs into F7 modules.
Dissertations, Reports and Manuscripts
Proving Cryptographic C Programs Secure with General-Purpose Verification Tools, Ph.D. Thesis, supervised by Andrew D. Gordon, Jan Jürjens and Bashar Nuseibeh.
Submitted in September 2012. Examined in February 2013 by Graham Steel and Yijun Yu. Corrections accepted in April 2013.
- Code and Proof Obfuscation, M.Sc. Thesis, supervised by David Pichardie.
- Deforestation of Functional Programs, B.Sc. Thesis, supervised by Robin Cockett.
- Using the syntactic construction of verbs to determine the semantic importance of their complements, undergraduate Thesis, supervised by Mehdi Yousfi-Monod and Augusta Mela.