Francois Dupressoir

Dr François Dupressoir

Lecturer in Secure Systems
+44 (0)1483 689195
https://fdupress.net
17 BB 02
MSc Personal Tutoring: Wed 10:00-12:00; Teaching: Tue 14:00-16:00

About

Areas of specialism

Machine-checked proofs; Security and Privacy; Formal Verification; Cryptography

University roles and responsibilities

  • Academic Integrity Officer
  • MSc Coordinator
  • MSc Admissions Tutor

    Research

    Research interests

    Publications

    Barthe G, Belaïd S, Dupressoir FSP, Fouque P-A, Grégoire B, Strub P-Y, Zucchini R (2016) Strong Non-Interference and Type-Directed Higher-Order Masking, CCS '16 - Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Securitypp. 116-129 ACM
    DOI: 10.1145/2976749.2978427
    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.
    Almeida JB, Barbosa M, Barthe G, Dupressoir FSP (2016) Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC, Fast Software Encryption - 23rd International Conference, FSE 2016 Bochum, Germany, March 20?23, 2016 Revised Selected Paperspp. 163-184 Springer Nature
    DOI: 10.1007/978-3-662-52993-5_9
    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, once reinforced, provides adequate mitigation against current adversary capabilities ? its existence serves as further evidence to the fact that conventional software validation processes are not effective in the study and validation of security properties. 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.
    Almeida J, Barbosa M, Barthe G, Dupressoir F, Grégoire B, Laporte V, Pereira V (2017) A Fast and Verified Software Stack for Secure Function Evaluation,CCS '17 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security Association for Computing Machinery (ACM)
    DOI: 10.1145/3133956.3134017
    We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao?s SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012).We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.
    Baritel-Ruet Cécile, Dupressoir Francois, Fouque Pierre-Alain, Grégoire Benjamin (2018) Formal Security Proof of CMAC and its Variants,Proceedings of the 31st IEEE Computer Security Foundations Symposium Institute of Electrical and Electronics Engineers (IEEE)
    DOI: 10.1109/CSF.2018.00014
    The CMAC standard, when initially proposed by Iwata and Kurosawa as OMAC1, was equipped with a complex game-based security proof. Following recent advances in formal verification for game-based security proofs, we formalize a proof of unforgeability for CMAC in EasyCrypt. A side effect of this proof includes improvements and extensions to EasyCrypt?s standard libraries. This formal proof obtains security bounds very similar to Iwata and Kurosawa?s for CMAC, but also proves secure a certain number of intermediate constructions of independent interest, including ECBC, FCBC and XCBC. This work represents one more step in the direction of obtaining a reliable set of independently verifiable evidence for the security of international cryptographic standards.
    Cortier Véronique, Dragan Constantin C?t?lin, Dupressoir Francois, Warinschi Bogdan (2018) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios,Proceedings of the 31st IEEE Computer Security Foundations Symposium Institute of Electrical and Electronics Engineers (IEEE)
    DOI: 10.1109/CSF.2018.00029
    We present a machine-checked security analysis of Belenios ? a deployed voting protocol used already in more than 200 elections. Belenios extends Helios with an explicit registration authority to obtain eligibility guarantees. We offer two main results. First, we build upon a recent framework for proving ballot privacy in EasyCrypt. Inspired by our application to Belenios, we adapt and extend the privacy security notions to account for protocols that include a registration phase. Our analysis identifies a trust assumption which is missing in the existing (pen and paper) analysis of Belenios: ballot privacy does not hold if the registrar misbehaves, even if the role of the registrar is seemingly to provide eligibility guarantees. Second, we develop a novel framework for proving strong verifiability in EasyCrypt and apply it to Belenios. In the process, we clarify several aspects of the pen-and-paper proof, such as how to deal with revote policies. Together, our results yield the first machine-checked analysis of both ballot privacy and verifiability properties for a deployed electronic voting protocol. Perhaps more importantly, we identify several issues regarding the applicability of existing definitions of privacy and verifiability to systems other than Helios. While we show how to adapt the definitions to the particular case of Belenios, our findings indicate the need for more general security notions for electronic voting protocols with registration authorities.
    Almeida José Bacelar, Baritel-Ruet Cécile, Barbosa Manuel, Barthe Gilles, Dupressoir François, Grégoire Benjamin, Laporte Vincent Laporte, Oliveira Tiago, Stoughton Alley, Strub Pierre-Yves (2019) Machine-Checked Proofs for Cryptographic Standards,CIS '19 Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS 2019)pp. 1607-1622 Association for Computing Machinery (ACM)
    DOI: 10.1145/3319535.3363211

    We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive.

    Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.