Journal Publications and Book Chapters

ComputerAided Proofs in Cryptography: An overview, with Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt and PierreYves Strub.
All about Proofs, Proofs for All. Vol 55. Mathematical Logic and Foundations. 2015.
A brief introduction to some of the recent developments in computeraided cryptography, including CertiCrypt, EasyCrypt, ZooCrypt and more specialized tools.

Guiding a GeneralPurpose C Verifier to Prove Cryptographic Protocols, with Andrew D. Gordon, Jan Jürjens and David A. Naumann.
Journal of Computer Security. 22(5):823866, 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 PierreYves 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 NonInterference and TypeDirected HigherOrder Masking, with Gilles Barthe, Sonia Belaïd, PierreAlain Fouque, Benjamin Grégoire, PierreYves 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 sidechannel 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.
Preliminary Version (external)  CameraReady [.pdf]
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 stateoftheart. 
Verifying ConstantTime Implementations, with José Bacelar Almeida, Manuel Barbosa, Gilles Barthe and Michael Emmi.
In 25th USENIX Security Symposium (USENIX Security 2016), pages 5370.
The constanttime programming discipline is an effective countermeasure against timing and cachetiming 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 constanttime code an essential component for building secure software. We propose a novel approach, based on the construction of a selective product program, for verifying constanttime security of realworld code, including implementations that locally and intentionally violate strict constanttime 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, ctverif, that leverages the Smack and Boogie tools and verifies constanttime properties of optimized LLVM code, thereby removing the main part of the compiler from the TCB for sidechannel security. We present verification results obtained over a wide range of constanttime components, from cryptographic (NaCl, FourQLib, OpenSSL, ...) and noncryptographic (libfixedtimefixedpoint, ...) offtheshelf libraries.
Open Access Proceedings (external) 
Verifiable sidechannel security of cryptographic implementations: constanttime MEECBC, with José Bacelar Almeida, Manuel Barbosa and Gilles Barthe.
In 23rd International Conference on Fast Software Encryption (FSE 2016), pages 163184. Best paper award.
We provide further evidence that implementing software countermeasures against timing attacks is a nontrivial task and requires domainspecific 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 MACthenEncodethenCBCEncrypt (MEECBC) component, creating a timing sidechannel similar to that exploited by Lucky 13. Although such an attack could only be launched when the MEECBC 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 blackbox 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 proofofconcept application of our methodology to MEECBC, 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 sidechannel 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.
ePrint (external)  Springer (external) 
Verified Proofs of HigherOrder Masking, with Gilles Barthe, Sonia Belaïd, PierreAlain Fouque, Benjamin Grégoire and PierreYves Strub.
In Advances in Cryptology  EUROCRYPT 2015  34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, pages 457485.
In this paper, we study the problem of automatically verifying higherorder masking countermeasures. This problem is important in practice (weaknesses have been discovered in schemes that were thought secure), but is inherently exponential: for torder 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 higherorder 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 languagebased 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.
ePrint (external)  Springer (external) 
Synthesis of Fault Attacks on Cryptographic Implementations, with Gilles Barthe, PierreAlain Fouque, Benjamin Grégoire and JeanChristophe Zapalowicz.
In Proceedings of the 2014 ACM SIGSAC conference on Computer & Communications Security (CCS 2014), pages 10161027.
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 highlevel 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, toolsupported 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 implementationindependent 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 latticebased 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.
ACM AuthorIzer (external)  ePrint (external) 
Making RSAPSS Secure Against Random Faults, with Gilles Barthe, Benjamin Grégoire, PierreAlain Fouque, Mehdi Tibouchi and JeanChristophe Zapalowicz.
In Proceedings of the 2014 Workshop on Cryptographic Hardware and Embedded Systems (CHES 2014), pages 206222.
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 nonrandom 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 nonrandom 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 nonrandom 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.
ePrint (external)  Associated Material [.tar.bz2] 
Certified ComputerAided Cryptography: Efficient Provably Secure Machine Code from HighLevel 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 12171230.
We present a computeraided framework for proving concrete security bounds for cryptographic machine code implementations. The frontend of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of Clike programs extended with idealised probabilistic operations in the style of codebased 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 highlevel, and is also instrumented to detect when compilation may interfere with sidechannel countermeasures deployed in source code. We demonstrate the applicability of the framework with the RSAOAEP 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 computeraided cryptographic tools to realworld security, and the first application of CompCert to cryptographic software.
ACM AuthorIzer (external)  ePrint (external) 
Guiding a GeneralPurpose 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 317.
We describe how to verify security properties of C code for cryptographic protocols by using a generalpurpose 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 generalpurpose 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.
Tech Report (external)  Preprint [.pdf]  Sample Code [tar.gz]  Short slide deck [.pdf]  Full slide deck [.pdf]
NonRefereed Publications
 Compositional Verification of HigherOrder Masking: Application to a Verifying Masking Compiler, with Gilles Barthe, Sonia Belaïd, PierreAlain Fouque, Benjamin Grégoire and PierreYves Strub. ePrint (external)
 Verified Implementations for Secure and Verifiable Computation, with José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, Benjamin Grégoire and PierreYves Strub. ePrint (external)
 Proving Computational Security with a GeneralPurpose C Verifier, with Cédric Fournet and Andrew D. Gordon. FCC 2012 and ASA6, Harvard University, June 2012. Talk proposal [.pdf]  Slide Deck [.pptx]

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 verificationcondition 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 twomessage protocol.

Verifying Authentication Properties of C Security Protocol Code Using GeneralPurpose Verifiers, with Andrew D. Gordon and Jan Jürjens.
ASA4, 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.
Extended abstract [.pdf]  Slides [.pdf]
Dissertations, Reports and Manuscripts

Proving Cryptographic C Programs Secure with GeneralPurpose 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. Thesis [.pdf]  Companion Archive [.zip]  Code and Proof Obfuscation, M.Sc. Thesis, supervised by David Pichardie. Thesis [.pdf]  Bibliographic Report [.pdf] (in French)
 Deforestation of Functional Programs, B.Sc. Thesis, supervised by Robin Cockett. Thesis [.pdf]
 Using the syntactic construction of verbs to determine the semantic importance of their complements, undergraduate Thesis, supervised by Mehdi YousfiMonod and Augusta Mela. Thesis [.pdf] (in French)