The main countermeasure against side-channel attacks is masking, which aims to remove the correlation between the handled data and the physical quantities that can be measured by transforming the computation.
Sensitive data is split into shares using uniformly distributed randomly generated values and are always used in the computation in such a way that not all shares are used at the same time, thus removing the correlation between sensitive values and physical quantities. Masking is hard to implement but can be verified to be correctly implemented, in a given "leakage model".
This model represents the information that can be retrieved by an attacker doing measurements on the running circuit.
State-of-the-art leakage models account for hardware side-effects such as transitions and glitches, to obtain verification verdicts closer to the leakage observed in practice.
This PhD thesis focuses on the verification of masking of hardware accelerators and software executed by general-purpose processors.
A new formal method of verification implemented in a tool named aLEAKator is presented, making use of "mixed-domain simulation" of hardware descriptions of circuits. aLEAKator is open-source, allows for the verification in various leakage models, is able to verify programs making use of precomputed tables and introduces the notion of verification granularity, previously missing from the state-of-the-art.
The method is validated by reproducing existing verification verdicts from the state-of-the-art and by providing new results on software implementations and cycle-by-cycle comparison of verdict with real measurements of widely deployed processors.
Finally, cryptographic functions that were not verified in complex leakage models in the past such as AES masked with Herbst scheme are verified in this PhD thesis on five different processors with both RISC-V and ARMv7-M architectures.
Moreover, this PhD thesis provides an inventory of common hardware leakage sources on general-purpose processors. Additionally, countermeasures against these sources are provided and validated with real measurements.
A method to automatically eradicate leakages from software executed on processors by making use of the detailed leakage nature and origin report of aLEAKator is then presented. This method is applied to the ARM Cortex-M4 processor and allows for the hardening of several software implementations in the presence of glitches and transitions. Notably, this method was used on the AES masked with the Herbst scheme, allowing for the first implementation, to the best of our knowledge, of this cipher on these leakage models.