• [papers]
  • [talks]
  • [phd]

    • The difference between theory and practice is that in theory there is none.

    Emancipatory security and privacy

    I define myself as a researcher in emancipatory security and privacy. That is, methods and tools that give people (rather than companies or states) control over their personal data and more generally over the technologies they use. I'm a member of the PASTIS research team, and my research takes place in multiple contexts: the Upsilon project, which I launched in 2019 with François Lesueur; the Géode project, which is carried by the Institut Français de Géopolitique; the GdR “Internet, IA et Société”, which is carried by the Centre Internet et Société

    Limits of blockchains

    A blockchain is the solution to a very particular problem: solving distributed consensus in a fully adversarial setting. Apart from crypto-currencies, which can do without trusted third parties because transactions are performative writings on their blockchain, no other use-case exist that need to solve the specific problem that blockchains tackle. Nonetheless, the hype surrounding this technology is so strong that blockchains seem to be everywhere while being seldom necessary nor efficient. The use of blockchains is even encouraged by some actors in a number of contexts (voting, health, education, traceability, humanitarian aid, …) where there can be political issues, endangering democracy and freedom. I aim to make all these issues very clear and accessible to all types of audiences, from academics to the general public.

    Check out my papers (below), blog posts, and conferences on this subject.
    → Stay tuned at pablockchain.fr.

    Formal model for privacy as control

    Rather than the right to be let alone, as originally defined by Samuel Warren and Louis Brandeis in their famous article, privacy is increasingly seen in the digital society as the ability for individuals to control their personal data. The current trend is also to recommend the integration of privacy requirements in the earliest stages of the design of a product, following the privacy by design approach. However, even if the notions of privacy as control and privacy by design are predominant in the privacy literature, clear definitions of their meanings are still missing. As a result, they can be interpreted in different ways and it is difficult to make their implementation systematic and measurable.

    As a first step to address this issue, my goal is to study the notion of control over personal data, analyze its similarities and differences with existing notions such as access control or usage control and, based on previous work in these areas, propose a formal model for control over personal data. This formal model could serve as a basis for implementations including a combination of a priori controls (static, or dynamic through monitoring) and a posteriori controls.

    This joint work with Daniel Le Métayer lead to the Capacity framework, which allows to formally model, characterize, and evaluate control. See the Capacity paper below.

    Tools for usable privacy as control

    The goal of the Tupac research project is to empower people with more control over their personal data. In previous work with Daniel Le Métayer, we laid the necessary theoretical foundation to undertake this challenge. Three dimensions of control have been identified, which correspond to the capacities for an individual: to perform actions on their personal data, to prevent others from performing actions on their personal data, and to be informed of actions performed by others on their personal data. Based on this we built Capacity, a framework to formally model, characterize, and evaluate control, and thus, privacy.

    Now, this project aims at building actual tools based on Capacity. These tools should be usable by all actors, not only computer science researchers trained in formal methods: lawyers and engineers (typically those working for data controllers and data processors), but also and more importantly, final users. Indeed, trust and informed (lack of) consent are key to control, and while I'm clearly not in favor of “technological solutionism”, I believe we can improve privacy by giving people tools that help them better understand and evaluate the control they can have over their personal data, and the impact on this control of the decisions they can make. The same tools could also be used by developers to guide their implementation choices in favor of privacy by design.

    More details on the Tupac project.

    Parts of the Tupac project are being worked on by Sylvain Chichery as a postdoc funded by the ReComp project, which aims at enhancing the reliability of AI in society by implementing real-time compliance mechanism for legal and ethical norms, including concerning personal data.

    Trustable homomorphic computation

    Homomorphic cryptography is used when computations are delegated to an untrusted third-party. However, there is a discrepancy between the untrustworthiness of the third-party and the silent assumption that it will perform the expected computations on the encrypted data. This can be quite bothersome concerning privacy when homomorphic cryptography is used to outsource resources-greedy computations on personal data (e.g., from an IoT device to the cloud). By leveraging the methods developed to protect embedded asymmetric cryptography computations against fault injection attack, it should be possible to cost-effectively verify that the sequence of operations executed by the untrusted third-party actually corresponds to what was expected.

    The goal of the THC project is to validate this idea both theoretically and experimentally, by studying the security properties of such an homomorphic computation scheme and implementing it in a proof-of-concept library. See the THC paper below.

    Publications

    Blockchain : une mauvaise solution à la recherche d'un problème 🔗

    On entend de plus en plus parler de nouvelles technologies telles que les « cryptomonnaies », le « métavers », les « NFT », ou encore le « web3 », et celles-ci sont invariablement présentées comme des innovations incontournables du monde de demain, sans que ne soit jamais vraiment expliqué ni pourquoi ni comment… sauf une chose : c'est grâce à « la blockchain » ! En plus de ces nouvelles technologies, « la blockchain » est censée également révolutionner certaines pratiques existantes : par exemple la certification de documents (notariat, diplômes) ou la traçabilité (supply chain, agro-industrie), et parfois même, la démocratie (vote électronique)… Après avoir rapidement expliqué les bases du fonctionnement d'une blockchain, nous partirons de cet état de fait technique pour se poser plusieurs questions : concrètement, ça fait quoi, une blockchain ? dans quelles hypothèses ? et du coup, quelles sont les limites de cette technologie ? mais alors, est-ce que ça résout un problème qui existe dans la vraie vie ?
    Nous répondrons à ces questions avec un focus sur un des usages que des personnes à la recherche d'un problème à résoudre avec une blockchain poussent énormément dans l'enseignement supérieur et la recherche : la certification de diplômes.
    En conclusion, nous reviendrons sur le caractère d’« innovation de rupture » systématiquement associé à cette technologie, et nous nous questionnerons sur son rôle en pratique, non plus techniquement, mais socialement et politiquement.

    Promesses et (dés)illusions : une introduction technocritique aux blockchains 🔗

    « Une blockchain est un registre distribué et immuable dans lequel sont écrites des informations qui font consensus. ». Dans cet article, nous commencerons par donner du sens à cette phrase et à l’ensemble des termes qui y sont employés, en nous efforçant quand c’est nécessaire de rendre accessibles les notions informatiques (comme la décentralisation, la distribution, l’immuabilité, ou le consensus) et le fonctionnement technique des outils cryptographiques sous-jacents (comme les condensats, les signatures, ou la preuve de travail ou d’enjeu). L’objectif de cette introduction sera d’atteindre une compréhension réelle de ce qu’est une blockchain.
    Ainsi équipés, nous discuterons ensuite de ce que les blockchains permettent effectivement d’accomplir, et donc surtout ce qu’elles ne permettent pas. Nous questionnerons alors les utilisations qui en sont proposées en nous concentrant sur des cas d’usage typiques des blockchains que nous étudierons plus en détails : les « cryptomonnaies » bien sûr, la certification de documents (avec l’exemple des diplômes), et nous mentionnerons également le cas des NFT. Cela nous permettra en conclusion de questionner de manière générale le caractère d’« innovation de rupture » que l’on associe souvent à cette technologie.

    Auteur·ices, relecteur·ices : redoublons de prudence face aux effets de modes technologiques 🔗
    • Rapport 2022.

    Dans un article paru dans Amplitude du droit le 21 juin 2022, le juriste Serge Surin élabore une défense du vote électronique reposant sur la chaîne de blocs (CDB) ou blockchain. Cet article commet de nombreuses erreurs méthodologiques, notamment par sa gestion des sources — utilisation non critique de propagande d'État et de produits publicitaires — ainsi que par une certaine incompréhension des technologies étudiées. Ayant l'habitude de travailler aux interfaces disciplinaires, nous souhaitons sonner l'alarme sur de telles pratiques, facilitées par l'analyse d'un outil technologique sans collaborer avec les personnes ayant l'expertise nécessaire. Nous proposons donc ici une critique et une réfutation détaillée, et interrogeons la rigueur du mécanisme d'évaluation par les pairs censé avoir eu lieu.

    THC: Practical and Cost-Effective Verification of Delegated Computation 🔗

    Homomorphic cryptography is used when computations are delegated to an untrusted third-party. However, there is a discrepancy between the untrustworthiness of the third-party and the silent assumption that it will perform the expected computations on the encrypted data. This may raise serious privacy concerns, for example when homomorphic cryptography is used to outsource resource-greedy computations on personal data (e.g., from an IoT device to the cloud). In this paper we show how to cost-effectively verify that the delegated computation corresponds to the expected sequence of operations, thus drastically reducing the necessary level of trust in the third-party. Our approach is based on the well-known modular extension scheme: it is transparent for the third-party and it is not tied to a particular homomorphic cryptosystem nor depends on newly introduced (and thus less-studied) cryptographic constructions. We provide a proof-of-concept implementation, THC (for trustable homomorphic computation), which we use to perform security and performance analyses. We then demonstrate its practical usability, in the case of a toy electronic voting system.

    SeseLab : une plateforme logicielle pour l'enseignement des attaques physiques 🔗

    L'actualité de la sécurité informatique ne manque pas de nous rappeler la nécessité de faire part à nos étudiant·e·s de la puissance des attaques par canaux auxiliaires, y compris dans les formations qui ne sont pas concentrées sur la sécurité. Dans le cadre d'un cours d'introduction à la sécurité des systèmes embarqués, j'ai voulu faire expérimenter ces attaques aux étudiant·e·s. Le matériel nécessaire à la mise en œuvre d'une attaque physique, en plus d'être coûteux et encombrant, nécessiterait un apprentissage spécifique et donc un encadrement conséquent. Pour pallier ces soucis, je présente ici SeseLab, une plateforme entièrement logicielle utilisable dans des salles de TP classiques, permettant tout de même aux étudiant·e·s de simuler des attaques physiques sur des implémentations cryptographiques.

    Capacity: an Abstract Model of Control over Personal Data 🔗

    While the control of individuals over their personal data is increasingly seen as an essential component of their privacy, the word “control” is usually used in a very vague way, both by lawyers and by computer scientists. This lack of precision may lead to misunderstandings and makes it difficult to check compliance. To address this issue, we propose a formal framework based on capacities to specify the notion of control over personal data and to reason about control properties. We illustrate our framework with social network systems and show that it makes it possible to characterize the types of control over personal data that they provide to their users and to compare them in a rigorous way.

    Dictionnaire des bien communs — Entrée “Publication en libre accès” 🔗

    Contribution de l'entrée “Publication en libre accès” dans le Dictionnaire des biens communs, publié chez PUF sous la direction de Marie Cornu, Fabienne Orsi, et Judith Rochfeld.

    Guide to Pairing-Based Cryptography — Chapter 12: Physical Attacks 🔗

    “This book is devoted to efficient pairing computations and implementations, useful tools for cryptographers working on topics like identity-based cryptography and the simplification of existing protocols like signature schemes.”
    Our chapter (the twelfth and last one) covers physical attacks and countermeasures.

    Using Modular Extension to Provably Protect Edwards Curves Against Fault Attacks 🔗

    Fault injection attacks are a real-world threat to cryptosystems, in particular asymmetric cryptography. In this paper, we focus on countermeasures which guarantee the integrity of the computation result, hence covering most existing and future fault attacks. Namely, we study the modular extension protection scheme in previously existing and newly contributed variants of the countermeasure on elliptic curve scalar multiplication (ECSM) algorithms. We find that an existing countermeasure is incorrect and we propose new “test-free” variant of the modular extension scheme that fixes it. We then formally prove the correctness and security of modular extension: specifically, the fault non-detection probability is inversely proportional to the security parameter. Finally, we implement an ECSM protected with test-free modular extension during the elliptic curve operation to evaluate the efficient of this method on Edwards and twisted Edwards curves.

    Algorithmic Countermeasures Against Fault Attacks and Power Analysis for RSA-CRT 🔗

    In this work, we analyze all existing RSA-CRT countermeasures against the Bellcore attack that use binary self-secure exponentiation algorithms. We test their security against a powerful adversary by simulating fault injections in a fault model that includes random, zeroing, and skipping faults at all possible fault locations. We find that most of the countermeasures are vulnerable and do not provide sufficient security against all attacks in this fault model. After investigating how additional measures can be included to counter all possible fault injections, we present three countermeasures which prevent both power analysis and many kinds of fault attacks.

    High Precision Fault Injections on the Instruction Cache of ARMv7-M Architectures 🔗

    Hardware and software of secured embedded systems are prone to physical attacks. In particular, fault injection attacks revealed vulnerabilities on the data and the control flow allowing an attacker to break cryptographic or secured algorithms implementations. While many research studies concentrated on successful attacks on the data flow, only a few targets the instruction flow. In this paper, we focus on electromagnetic fault injection (EMFI) on the control flow, especially on the instruction cache. We target the very widespread (smartphones, tablets, settop-boxes, health-industry monitors and sensors, etc.) ARMv7-M architecture. We describe a practical EMFI platform and present a methodology providing high control level and high reproducibility over fault injections. Indeed, we observe that a precise fault model occurs in up to 96% of the cases. We then characterize and exhibit this practical fault model on the cache that is not yet considered in the literature. We comprehensively describe its effects and show how it can be used to reproduce well known fault attacks. Finally, we describe how it can benefits attackers to mount new powerful attacks or simplify existing ones.

    Countermeasures Against High-Order Fault-Injection Attacks on CRT-RSA 🔗

    In this paper we study the existing CRT-RSA countermeasures against fault-injection attacks. In an attempt to classify them we get to deeply understand the way they work. We show that the many countermeasures (and their variations) that we study actually share a number of common features, but optimize them in different ways. We also show that there is no conceptual distinction between test-based and infective countermeasures and how it is possible to transform one into the other (or vice versa). Furthermore, we show that faults on the code (skipping instructions) can be captured by considering only faults on the data. These intermediate results allow us to improve the state of the art in several ways: (a) we fix an existing and known to be broken countermeasure (namely the one from Shamir); (b) we drastically optimize an existing countermeasure (namely the one from Vigilant) which we reduce to 3 tests instead of 9 in its original version, and prove that it resists not only one fault but also an arbitrary number of randomizing faults; (c) we also show how to upgrade countermeasures to resist any given number of faults: given a correct first-order countermeasure, we present a way to design a provable high-order countermeasure (for a well-defined and reasonable fault model). Finally, we pave the way for a generic approach against fault attacks for any modular arithmetic computations, and thus for the automatic insertion of countermeasures.

    Formally Proved Security of Assembly Code Against Power Analysis 🔗

    In his keynote speech at CHES 2004, Kocher advocated that side-channel attacks were an illustration that formal cryptography was not as secure as it was believed because some assumptions (e.g., no auxiliary information is available during the computation) were not modeled. This failure is caused by formal methods' focus on models rather than implementations. In this paper we present formal methods and tools for designing protected code and proving its security against power analysis. These formal methods avoid the discrepancy between the model and the implementation by working on the latter rather than on a high-level model. Indeed, our methods allow us (a) to automatically insert a power balancing countermeasure directly at the assembly level, and to prove the correctness of the induced code transformation; and (b) to prove that the obtained code is balanced with regard to a reasonable leakage model, and we show how to characterize the hardware to use the resources which maximize the relevancy of the model. The tools implementing our methods are then demonstrated in a case study in which we generate a provably protected PRESENT implementation for an 8-bit AVR smartcard.

    Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack 🔗

    In our paper at PROOFS 2013, we formally studied a few known countermeasures to protect CRT-RSA against the BellCoRe fault injection attack. However, we left Vigilant's countermeasure and its alleged repaired version by Coron et al. as future work, because the arithmetical framework of our tool was not sufficiently powerful. In this paper we bridge this gap and then use the same methodology to formally study both versions of the countermeasure. We obtain surprising results, which we believe demonstrate the importance of formal analysis in the field of implementation security. Indeed, the original version of Vigilant's countermeasure is actually broken, but not as much as Coron et al. thought it was. As a consequence, the repaired version they proposed can be simplified. It can actually be simplified even further as two of the nine modular verifications happen to be unnecessary. Fortunately, we could formally prove the simplified repaired version to be resistant to the BellCoRe attack, which was considered a challenging issue by the authors of the countermeasure themselves.

    A Formal Proof of Countermeasures Against Fault Injection Attacks on CRT-RSA 🔗

    In this article, we describe a methodology that aims at either breaking or proving the security of CRT-RSA implementations against fault injection attacks. In the specific case-study of the BellCoRe attack, our work bridges a gap between formal proofs and implementation-level attacks. We apply our results to three implementations of CRT-RSA, namely the unprotected one, that of Shamir, and that of Aumüller et al. Our findings are that many attacks are possible on both the unprotected and the Shamir implementations, while the implementation of Aumüller et al. is resistant to all single-fault attacks. It is also resistant to double-fault attacks if we consider the less powerful threat-model of its authors.

    From Rational Number Reconstruction to Set Reconciliation and File Synchronization 🔗

    This work revisits set reconciliation, the problem of synchronizing two multisets of fixed-size values while minimizing transmission complexity. We propose a new number-theoretic reconciliation protocol called Divide and Factor (D&F) that achieves optimal asymptotic transmission complexity — as do previously known alternative algorithms. We analyze the computational complexities of various D&F variants, study the problem of synchronizing sets of variable-size files using hash functions and apply D&F to synchronize file hierarchies taking file locations into account.
    We describe btrsync, our open-source D&F implementation, and benchmark it against the popular software rsync. It appears that btrsync transmits much less data than rsync, at the expense of a relatively modest computational overhead.

    Can a Program Reverse-Engineer Itself? 🔗

    Shape-memory alloys are metal pieces that “remember” their original cold-forged shapes and return to the pre-deformed shape after heating. In this work we construct a software analogous of shape-memory alloys: programs whose code resists obfuscation. We show how to pour arbitrary functions into protective envelops that allow recovering the functions' exact initial code after obfuscation. We explicit the theoretical foundations of our method and provide a concrete implementation in Scheme.

    Can Code Polymorphism Limit Information Leakage? 🔗

    In addition to its usual complexity assumptions, cryptography silently assumes that information can be physically protected in a single location. As one can easily imagine, real-life devices are not ideal and information may leak through different physical side-channels. It is a known fact that information leakage is a function of both the executed code F and its input x.
    In this work we explore the use of polymorphic code as a way of resisting side channel attacks. We present experimental results with procedural and functional languages. In each case we rewrite the protected code Fi before its execution. The outcome is a genealogy of programs F0, F1, … such that for all inputs x and for all indexes i ≠ j ⇒ Fi(x) = Fj(x) and Fi ≠ Fj. This is shown to increase resistance to side channel attacks.

    Selected Talks and Posters

    Students and Postdocs

    Service Activities

    PhD

    Formal Software Methods for Cryptosystems Implementation Security

    Implementations of cryptosystems are vulnerable to physical attacks, and thus need to be protected against them. Of course, malfunctioning protections are useless. Formal methods help to develop systems while assessing their conformity to a rigorous specification. The first goal of my thesis, and its innovative aspect, is to show that formal methods can be used to prove not only the principle of the countermeasures according to a model, but also their implementations, as it is where the physical vulnerabilities are exploited. My second goal is the proof and the automation of the protection techniques themselves, because handwritten security code is error-prone.
    Physical attacks can be classified into two distinct categories. Passive attacks, where the attacker only reads information that leaks through side channels (such as power consumption or electromagnetic emanations). And active attacks, where the attacker tampers with the system to have it reveal secrets through its “normal” output channel. Therefore, I have pursued my goals in both settings: on a countermeasure that diminishes side-channel leakage, and on countermeasures which detect fault injection attacks.

    Defense (2015-07-13)

    Files: thesis (also on TEL) and presentation slides.
    Advisor: Sylvain Guilley.
    Referees: Pierre-Alain Fouque and Marie-Laure Potet.
    Examiners: François Dupressoir, Karine Heydemann, David Naccache (president), Mehdi Tibouchi, and David Vigilant.

    Midterm defense (2013-12-04)

    Files: report and presentation slides.
    Jury: Karine Heydemann and Jean Goubault-Larrecq.

    Undergraduate Research

    Mixing Continuous and Discrete Time in a Synchronous Language

    March to August 2012, in the ENS/Inria Parkas team in Paris (France).

    A hybrid system is a system that exhibits both discrete and continous behaviors (e.g., a programmed controller and the evolution of its environment). Zélus is a hybrid synchronous programming language, allowing the programmation and modelization of hybrid systems. The modelization of hybrid systems works by alternating between continuous phases and discrete steps. During continuous phases the continuous state of the system evolves in time with respect to differential equations. At discrete steps the discrete state of the system may change instantaneously.
    The main result of this report is a static analysis of Zélus code which detects if there can be an infinite number of discrete steps between two continuous phases. The presence of a finite number of such steps is a necessary condition to ensure time progress during a simulation of the system.
    The question of the automatic translation of hybrid automata, a formalism to analyze/modelize hybrid systems, into Zélus code, is also raised. Small results in this direction are shown and then a roadmap for pursuing this translation is proposed.

    Implicit parallelization of code called from an external and already parallelized environment

    April to August 2011, in the UvA Computer Systems Architecture group in Amsterdam (Netherlands).

    SAC is a purely functional array-based programming language with a strong focus on implicit parallelization. Our goal is to enable C programmers to take advantage of SAC implicit parallelization through SAC C interface. The difficulty however is that the SAC parallelization mechanism is not designed to be called from already parallelized programs. We aim at solving this problem by redesigning the SAC C interface, but with minimal changes to SAC's efficient implicit parallelization mechanism. To this end we extend the SAC compiler to introduce the concept of XT functions and virtual runtime environments. XT functions allow the implicit parallelization to take place in an already parallel context.

    A formal approach to the development of system services in embedded systems

    June to August 2010, in the Verimag Synchrone team in Grenoble (France).

    Our goal is to enable preemptive multitasking in critical embedded systems programmed with the formally defined Lustre programming language, in order to get rid of the constraints imposed by static scheduling, which is still in use at this day. We aim to do so by introducing a tiny system layer between the hardware and the software, which would also be written as much as possible in Lustre to allow global validation of the system using formal verification methods.