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 implementation, as it is very 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.
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 (such as power consumption or electromagnetic emanations),
and on countermeasures against fault injection attacks.
As there already exists a rigorous security property for protections against side-channel leakage, my contributions concentrate on formal methods for design and verification of protected implementations of algorithms.
I have developed a methodology to protect an implementation by generating an improved version of it which has a null side-channel signal-to-noise ratio, as its leakage is made constant (in particular, it does not depend on the secret values).
For the sake of demonstration, I have also undertaken to write a tool which automates the application of the methodology on an insecure input code written in assembly language.
Independently, the tool is able to prove that this constant leakage property holds for a given implementation, which can be used to verify the security of the output of the protection mechanism.
To my best knowledge, paioli is the first tool which can automatically protect an implementation against side-channel leakage by provably balancing its side-channel leakage.
In contrast, the very definition of the security objectives was not clearly established for fault injection attacks before I started my PhD.
Many countermeasures have been published without any proofs, as the necessary properties to prove were not formally expressed.
It is only during my PhD that so called ``attack success conditions'' were introduced.
Hence, the first question was to evaluate existing countermeasures with respect to these attack success conditions.
To this end, I have developed a theoretical framework and a tool implementing it.
The use of finja allowed me and others to verify some countermeasures, but also to find known attacks and discover new ones.
A second question was the minimality of the countermeasures.
I have studied in depth one of the state-of-the-art's countermeasure.
I have been able to drastically simplify it in terms of code length and randomness requirement, without affecting its security properties.
This work has shown the added value of formal methods, relative to engineering by trial-and-error like most countermeasures have been developed as of today.
Existing countermeasures claim to protect against one, or sometimes two, fault injections.
However, attacks using more than two faults have been shown practical.
The third question was then to create a new high-order countermeasure able to resist any number of faults.
In turn, the design of a new countermeasure raises the question of the accurate definition of the rational of countermeasures.
In a first step to find an answer, I have classified existing countermeasures in order to extract protection principles from the techniques they rely on.
This categorization work allowed me to understand the essence of a countermeasure.
Based on it, I have been able to propose a method for designing a countermeasure that can resists an arbitrary number of faults.
I have also noticed that all the countermeasures I have studied are variations of optimization for the same base technique consisting in verifying the integrity of the computation using a form of redundancy.
This technique is independent of the algorithm it is applied to and of the attack success conditions, as it only depends on the mathematical structure of the sensitive data, namely modular arithmetic.
I have thus proposed a property of resistance against fault injection attacks which goes beyond attack success conditions.
The fourth question was then to apply this technique to all asymmetric cryptography algorithms, which all use similarly structured data.
In order to achieve this goal, I have developed an abstraction of asymmetric cryptographic computations.
By design, this representation permits to apply the redundancy protection scheme.
I have formally defined this protection scheme by introducing a code transformation that I have proved correct.
I have written a compiler which automates this transformation and allowed to obtain protected implementations of cryptographic algorithms for which no countermeasures were known until now, but which were already victims of fault injection attacks.
An additional advantage of the enredo compiler is that it allows to study the trade-off between security and complexity.