VeriSiCC Seminar 2022

Presentation of a project partner

• Presentation of the VeriSiCC project

  Sonia Belaïd, CryptoExperts

Invited talk

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).

Coffee Break (30 min)

Presentation of a project partner

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.

Lunch Break (1h35)

Lunch is not provided but there are many restaurants next to the university

Invited Talk

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.

Presentation of a project partner

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

Coffee Break (30 min)

Invited Talk

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.

Closing remarks