The difference between theory and practice is that in theory there is none.
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.
My PhD thesis, and presentation slides (defended on 2015-07-13).
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.
My PhD midterm report,
(defended on 2013-12-04).
Jury: Karine Heydemann and Jean Goubault-Larrecq.
- 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
- PROOFS 2014: 3rd Workshop on Security Proofs for Embedded Systems
- JCEN: Journal of Cryptographic Engineering
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 issueby the authors of the countermeasure themselves.
- A Formal Proof of Countermeasures Against Fault Injection Attacks on CRT-RSA
- PROOFS 2013: 2nd Workshop on Security Proofs for Embedded Systems
- JCEN: Journal of Cryptographic Engineering
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
Séminaire SAS, 2015-03-19.
Protecting Against Fault Injection Attacks: from CRT-RSA to all Asymmetric Cryptography (slides).
- TRUDEVICE 2015, 2015-03-13.
Towards Generic Countermeasures Against Fault Injection Attacks (slides).
Rump session, Itinerant Crypto Seminars, at IMDEA 2015-01-22.
Towards Generic Countermeasures Against Fault Injection Attacks (slides).
9th Digital Security Day, "side channel attacks", at GDR SoC-SiP, 2014-12-04.
Power Analysis Immunity by Offsetting Leakage Intensity (slides).
- Formal Methods and Security seminar at Inria and DGA, 2014-03-14.
Formal Proofs of CRT-RSA Countermeasures Against the BellCoRe Attack (slides).
Poster session, CHES 2013, 2013-08-23.
Formally Proved Security of Assembly Code Against Leakage (poster).
- DigiCosme working group, 2013-07-10.
Formally Proved Security of Automatically Protected Software Against Physical Attacks (slides).
Short talk, COSADE 2013, 2013-03-08.
Software Countermeasures Against DPA Attacks (abstract, slides).
- 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.