Journal Publications

Refereed Conference Publications

  • 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'14), to appear.

    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'14), to appear.

    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.

    ePrint | Associated Material [.tar.bz2]
  • 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'13), pages 1217--1230. Berlin, November 2013.

    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.

    ACM Author-Izer | ePrint
  • 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'11), pages 3--17. Paris, June 2011.

    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.

    Tech Report (external) | Preprint [.pdf] | Sample Code [tar.gz] | Short slide deck [.pdf] | Full slide deck [.pdf]

Non-Refereed Publications

Dissertations, Reports and Manuscripts