The difference between theory and practice is that in theory there is none.
I'm working with Sylvain Guilley and Jean-Luc Danger on
formal software methods for cryptosystems implementation security.
More specifically, my goals are twofold:
first, I'd like to improve the automation of code and data protection against side-channel attacks
(by reducing as much as possible the information leakage through side-channels such as time, temperature, or power consumption)
using compilation techniques to formally prove the code transformation
(ensuring that the protection did not alter the semantic of the cryptographic algorithm);
second, I'd like to develop modelization methods and tools to help the formal study of side-channel and fault injection attacks, and especially the efficiency of countermeasures.
My PhD midterm report,
(defended on 2013-12-04).
Jury: Karine Heydemann and Jean Goubault-Larrecq.
Selected Talks and Posters
- Formal Methods and Security seminar, Formal Proofs of CRT-RSA Countermeasures Against the BellCoRe Attack.
- CHES 2013, Formally Proved Security of Assembly Code Against Leakage.
- COSADE 2013, Software Countermeasures Against DPA Attacks (abstract).
- 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 issueby the authors of the countermeasure themselves.
- A Formal Proof of Countermeasures Against Fault Injection Attacks on CRT-RSA
- PROOFS 2013: PROOFS: 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.
- 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.
- 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.