Dr François Dupressoir

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


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 interests

Courses I teach on

Postgraduate taught


My 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 Security pp. 116-129 ACM
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 Papers pp. 163-184 Springer Nature
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)
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)
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)
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)

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