VeriSiCC Seminar 2022 is a single-day seminar organized by all the partners of FUI25 VeriSiCC project and that will take place on Jussieu campus, Paris, France, on September, 22nd 2022.
Sincere thanks to LIP6 which graciously makes a room available for this event.
Cryptographic implementations are often vulnerable to side-channel attacks, which exploit the physical emanations of the underlying component to retrieve the manipulated secrets. The most widely used countermeasure today is masking, which aims to randomize the manipulated data. VeriSiCC project aims to build new methods to automatically verify and generate proven masked cryptographic implementations. This project relies on the multidisciplinarity of its consortium, ranging from researchers specializing in formal methods and side-channel attacks to end-users, to design innovative software tools with the support of SMEs. These tools will allow industrial people to develop safe and effective protected implementations by reaching a high level of certification and certification bodies (represented in the consortium by ANSSI) to quickly and accurately verify implementations submitted to evaluations.
This second seminar aims to bring together experts in the field of formal verification and side-channel countermeasures to get an overview of the state-of-the-art on this topic and to identify new challenges.
Registration is free but mandatory for physical attendance.
Session chair: Thomas Roche
Computer-Aided Hardware Security Verification
Pascal Sasdrich, Ruhr-Universität Bochum
Abstract. Modern cryptography provides a variety of tools and methods to develop robust cryptographic techniques as the foundation of security architectures. Regardless of this, established cryptographic schemes often have weaknesses in their practical and physical implementation that can be exploited by attackers. In particular, by observing or influencing physical characteristics of the executing electronic device, attackers can gain valuable information about processed sensitive data and undermine security.
In this context, the presentation discusses our research on computer-aided verification of hardware implementations against physical implementation attacks. More precisely, we will discuss concepts for information leakage verification (Side-Channel Analysis), information tampering verification (Fault-Injection Analysis), and combination of both approaches (Combined Attacks).
Session chair: Jean-Sébastien Coron
Random Probing Security: Towards Bridging the Gap Between Theory and Practice
Abdul Rahman Taleb, CryptoExperts and Sorbonne University
Abstract. Side-channel attacks exploit the physical leakage of a device executing cryptographic implementations to extract manipulated secrets. They can be built from cheap equipment and generally recover the keys in a limited time without specific protections. Since discovering these attacks in the late nineties, the community has investigated several approaches to counteract them. Among these approaches, masking is one of the most deployed in practice. The main idea of masking is to split the information between several variables called shares. An attacker must collect and aggregate the information from all these variables to recover sensitive data, which becomes exponentially hard with the number of shares as each observation comes with noise.
The community then introduced the concept of leakage models to theoretically reason on the security of such masked implementations. So far, the most widely used leakage model is the probing model defined by Ishai, Sahai, and Wagner (CRYPTO 2003), where we model the leakage as the exact values of t intermediate variables chosen by the attacker. While it is advantageous for security proofs, it does not capture an adversary exploiting full leakage traces, e.g., in horizontal attacks. Those attacks target the multiple manipulations of the same share to reduce noise and recover the corresponding value. Therefore, the community is focusing on more realistic leakage models, such as the random probing model. The leakage is assumed to gather the exact value carried out by each circuit wire with a probability of p. The security tightly reduces to the security in the noisy leakage model in which each variable leaks a noisy function of its value. The noisy leakage model is the closest to the reality of physical leakage but is less convenient for security proofs. The random probing model can also be extended to capture glitches or other side effects.
During this talk, I will briefly present the relations between the different leakage models and the main results that improve the security of existing constructions in the random probing model. Then, as manually verifying the security of such constructions is tedious in practice, I will present the verification techniques used to quickly and efficiently verify the security of small circuits. Namely, I will talk about our verification tool IronMask, one of the most efficient tools for verifying random probing security properties.
Session chair: Aurélien Greuet
Side-Channel Countermeasures for Lattice-Based Cryptography
Mélissa Rossi, ANSSI
Abstract. Lattice-based cryptography is considered as a quantum-safe alternative for the replacement of currently deployed schemes based on RSA and discrete logarithm on prime fields or elliptic
curves. It offers strong theoretical security guarantees, a large array of achievable primitives, and a competitive level of efficiency. For these reasons, several lattice-based cryptosystems have been chosen by NIST to be new international post-quantum standards. Hence, the study of the implementation security of these schemes is very relevant in anticipation of upcoming real world deployment.
This presentation will first introduce the post-quantum schemes in a high level and highlight several weak points in terms of side-channel security. Next, we will present some countermeasures techniques against timing attacks. In addition, we will detail masking techniques for lattice-based cryptography and the resulting performance penalty factor. Finally, we will briefly outline some new perspectives for automated verification of side-channel protection in the lattice domain.
Session chair: Romain Poussier
Side-channel Masking with Pseudo-Random Generator
Jean-Sébastien Coron, University of Luxembourg
Abstract. High-order masking countermeasures against side-channel attacks usually require plenty of randomness during their execution. For security against t probes, the classical ISW countermeasure requires O(t^2 s) random bits, where s is the circuit size. However running a True Random Number Generator (TRNG) can be costly in practice and become a bottleneck on embedded devices. In [IKL+13] the authors introduced the notion of robust pseudo-random number generator (PRG), which must remain secure even against an adversary who can probe at most t wires. They showed that when embedding a robust PRG within a private circuit, the number of random bits can be reduced to O(t^4), that is independent of the circuit size s (up to a logarithmic factor). Using bipartite expander graphs, this can be further reduced to O(t^(3+eps)); however the resulting construction is unpractical.
In this talk we describe a practical construction where the number of random bits is only O(t^2) for security against t probes, without expander graphs; moreover the running time of each pseudo-random generation goes down from O(t^4) to O(t). Our technique consists in using multiple independent PRGs instead of a single one. We show that for ISW circuits, the robustness property of the PRG is not required anymore, which leads to simple and efficient constructions. For example, for AES we only need 48 bytes of randomness to get second-order security (t=2), instead of 2880 in the original Rivain-Prouff countermeasure; when implemented on an ARM-based embedded device with a relatively slow TRNG, we obtain a 50% speed-up compared to Rivain-Prouff
Session chair: Benjamin Grégoire
Fine-Grained Power Leakage Models and Verification of Software Masking
Marc Gourjon, Hamburg University of Technology and NXP Semiconductors
Abstract. Constructing software implementations which are resilient against power side-channel attacks is a non-trivial task.
This is not only due to the difficulty of implementing the so-called masking countermeasure correctly but also due to the difficulty of "hardening", the process of mitigating all side-channel leakages which are specific to the device executing the implementation. The presentation discusses a general approach to assist the development of efficient and higher-order masked implementations based on user-supplied, fine-grained power leakage models expressed in a domain-specific language and automated verification methods to prove the resilience of assembly implementations secure against the device-specific leakage.