## CryptoDB

### Sonia Belaïd

#### Publications

**Year**

**Venue**

**Title**

2023

CRYPTO

Unifying Freedom and Separation for Tight Probing-Secure Composition
Abstract

The masking countermeasure is often analyzed in the probing model. Proving the probing security of large circuits at high masking orders is achieved by composing gadgets that satisfy security definitions such as non-interference (NI), strong non-interference (SNI) or free SNI. The region probing model is a variant of the probing model, where the probing capabilities of the adversary scale with the number of regions in a masked circuit. This model is of interest as it allows better reductions to the more realistic noisy leakage model. The efficiency of composable region probing secure masking has been recently improved with the introduction of the input-output separation (IOS) definition.
In this paper, we first establish equivalences between the non-interference framework and the IOS formalism. We also generalize the security definitions to multiple-input gadgets and systematically show implications and separations between these notions. Then, we study which gadgets from the literature satisfy these. We give new security proofs for some well-known arbitrary-order gadgets, and also some automated proofs for fixed-order, special-case gadgets. To this end, we introduce a new automated formal verification algorithm that solves the open problem of verifying free SNI, which is not a purely simulation-based definition. Using the relationships between the security notions, we adapt this algorithm to further verify IOS. Finally, we look at composition theorems. In the probing model, we use the link between free SNI and the IOS formalism to generalize and improve the efficiency of the tight private circuit (Asiacrypt 2018) construction, also fixing a flaw in the original proof. In the region probing model, we relax the assumptions for IOS composition (TCHES 2021), which allows to save many refresh gadgets, hence improving the efficiency.

2022

TCHES

High Order Side-Channel Security for Elliptic-Curve Implementations
Abstract

Elliptic-curve implementations protected with state-of-the-art countermeasures against side-channel attacks might still be vulnerable to advanced attacks that recover secret information from a single leakage trace. The effectiveness of these attacks is boosted by the emergence of deep learning techniques for side-channel analysis which relax the control or knowledge an adversary must have on the target implementation. In this paper, we provide generic countermeasures to withstand these attacks for a wide range of regular elliptic-curve implementations. We first introduce a framework to formally model a regular algebraic program which consists of a sequence of algebraic operations indexed by key-dependent values. We then introduce a generic countermeasure to protect these types of programs against advanced single-trace side-channel attacks. Our scheme achieves provable security in the noisy leakage model under a formal assumption on the leakage of randomized variables. To demonstrate the applicability of our solution, we provide concrete examples on several widely deployed scalar multiplication algorithms and report some benchmarks for a protected implementation on a smart card.

2021

EUROCRYPT

On the Power of Expansion: More Efficient Constructions in the Random Probing Model
📺
Abstract

The random probing model is a leakage model in which each wire of a circuit leaks with a given probability $p$. This model enjoys practical relevance thanks to a reduction to the noisy leakage model, which is admitted as the right formalization for power and electromagnetic side-channel attacks. In addition, the random probing model is much more convenient than the noisy leakage model to prove the security of masking schemes. In a recent work, Ananth, Ishai and Sahai (CRYPTO 2018) introduce a nice expansion strategy to construct random probing secure circuits. Their construction tolerates a leakage probability of $2^{-26}$, which is the first quantified achievable leakage probability in the random probing model. In a follow-up work, Bela\"id, Coron, Prouff, Rivain and Taleb (CRYPTO 2020) generalize their idea and put forward a complete and practical framework to generate random probing secure circuits. The so-called expanding compiler can bootstrap simple base gadgets as long as they satisfy a new security notion called \emph{random probing expandability} (RPE). They further provide an instantiation of the framework which tolerates a $2^{-8}$ leakage probability in complexity $\mathcal{O}(\kappa^{7.5})$ where $\kappa$ denotes the security parameter.
In this paper, we provide an in-depth analysis of the RPE security notion. We exhibit the first upper bounds for the main parameter of a RPE gadget, which is known as the \emph{amplification order}. We further show that the RPE notion can be made tighter and we exhibit strong connections between RPE and the \emph{strong non-interference} (SNI) composition notion. We then introduce the first generic constructions of gadgets achieving RPE for any number of shares and with nearly optimal amplification orders and provide an asymptotic analysis of such constructions. Last but not least, we introduce new concrete constructions of small gadgets achieving maximal amplification orders. This allows us to obtain much more efficient instantiations of the expanding compiler: we obtain a complexity of $\mathcal{O}(\kappa^{3.9})$ for a slightly better leakage probability, as well as $\mathcal{O}(\kappa^{3.2})$ for a slightly lower leakage probability.

2021

ASIACRYPT

Dynamic Random Probing Expansion with Quasi Linear Asymptotic Complexity
📺
Abstract

The masking countermeasure is widely used to protect cryptographic implementations against side-channel attacks. While many masking schemes are shown to be secure in the widely deployed probing model, the latter raised a number of concerns regarding its relevance in practice. Offering the adversary the knowledge of a fixed number of intermediate variables, it does not capture the so-called horizontal attacks which exploit the repeated manipulation of sensitive variables. Therefore, recent works have focused on the random probing model in which each computed variable leaks with some given probability p. This model benefits from fitting better the reality of the embedded devices. In particular, Belaïd, Coron, Prouff, Rivain, and Taleb (CRYPTO 2020) introduced a framework to generate random probing circuits. Their compiler somehow extends base gadgets as soon as they satisfy a notion called random probing expandability (RPE). A subsequent work from Belaïd, Rivain, and Taleb (EUROCRYPT 2021) went a step forward with tighter properties and improved complexities. In particular, their construction reaches a complexity of O(κ^{3.9}), for a κ-bit security, while tolerating a leakage probability of p = 2^{−7.5}.
In this paper, we generalize the random probing expansion approach by considering a dynamic choice of the base gadgets at each step in the expansion. This approach makes it possible to use gadgets with high number of shares –which enjoy better asymptotic complexity in the expansion framework– while still tolerating the best leakage rate usually obtained for small gadgets. We investigate strategies for the choice of the sequence of compilers and show that it can reduce the complexity of an AES implementation by a factor 10. We also significantly improve the asymptotic complexity of the expanding compiler by exhibiting new asymptotic gadget constructions. Specifically, we introduce RPE gadgets for linear operations featuring a quasi-linear complexity, as well as, an RPE multiplication gadget with linear number of multiplications. These new gadgets drop the complexity of the expanding compiler from quadratic to quasi-linear.

2020

EUROCRYPT

Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations
📺
Abstract

Cryptographic implementations deployed in real world devices often aim at (provable) security against the powerful class of side-channel attacks while keeping reasonable performances. Last year at Asiacrypt, a new formal verification tool named tightPROVE was put forward to exactly determine whether a masked implementation is secure in the well-deployed probing security model for any given security order t. Also recently, a compiler named Usuba was proposed to automatically generate bitsliced implementations of cryptographic primitives.
This paper goes one step further in the security and performances achievements with a new automatic tool named Tornado. In a nutshell, from the high-level description of a cryptographic primitive, Tornado produces a functionally equivalent bitsliced masked implementation at any desired order proven secure in the probing model, but additionally in the so-called register probing model which much better fits the reality of software implementations. This framework is obtained by the integration of Usuba with tightPROVE+, which extends tightPROVE with the ability to verify the security of implementations in the register probing model and to fix them with inserting refresh gadgets at carefully chosen locations accordingly.
We demonstrate Tornado on the lightweight cryptographic primitives selected to the second round of the NIST competition and which somehow claimed to be masking friendly. It advantageously displays performances of the resulting masked implementations for several masking orders and prove their security in the register probing model.

2020

CRYPTO

Random Probing Security: Verification, Composition, Expansion and New Constructions
📺
Abstract

Masking countermeasure is among the most powerful countermeasures to counteract side-channel attacks. Leakage models have been exhibited 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 at (CRYPTO 2003). While it is advantageously convenient for security proofs, it does not capture an adversary exploiting full leakage traces as, e.g., in horizontal attacks. Those attacks target the multiple manipulation of the same share to average a constant noise and recover the corresponding value. To capture a wider class of attacks another model was introduced and is referred to as the random probing model. From a leakage parameter p, each wire of the circuit leaks its value with probability p. While this model much better reflects the physical reality of side channels, it requires more complex security proofs and does not yet come with practical constructions.
In this paper, we define the first framework dedicated to the random probing model. We provide an automatic tool, called VRAPS, to quantify the random probing security of a circuit from its leakage probability. We also formalize a composition property for secure random probing gadgets and exhibit its relation to the strong non-interference (SNI) notion used in the context of probing security. We then revisit the expansion idea proposed by Ananth, Ishai, and Sahai (CRYPTO 2018) and introduce a compiler that builds a random probing secure circuit from small base gadgets achieving a random probing expandability property. We instantiate this compiler with small gadgets for which we verify the expected properties directly from our automatic tool. Our construction can tolerate a leakage probability up to 2^−8, against 2^−25 for the previous construction, with a better asymptotic complexity.

2018

ASIACRYPT

Tight Private Circuits: Achieving Probing Security with the Least Refreshing
Abstract

Masking is a common countermeasure to secure implementations against side-channel attacks. In 2003, Ishai, Sahai, and Wagner introduced a formal security model, named $$t$$-probing model, which is now widely used to theoretically reason on the security of masked implementations. While many works have provided security proofs for small masked components, called gadgets, within this model, no formal method allowed to securely compose gadgets with a tight number of shares (namely, $$t+1$$) until recently. In 2016, Barthe et al. filled this gap with maskComp, a tool checking the security of masking schemes composed of several gadgets. This tool can achieve provable security with tight number of shares by inserting mask-refreshing gadgets at carefully selected locations. However the method is not tight in the sense that there exists some compositions of gadgets for which it cannot exhibit a flaw nor prove the security. As a result, it is overconservative and might insert more refresh gadgets than actually needed to ensure $$t$$-probing security. In this paper, we exhibit the first tool, referred to as tightPROVE, able to clearly state whether a shared circuit composed of standard gadgets (addition, multiplication, and refresh) is $$t$$-probing secure or not. Given such a composition, our tool either produces a probing-security proof (valid at any order) or exhibits a security flaw that directly implies a probing attack at a given order. Compared to maskComp, tightPROVE can drastically reduce the number of required refresh gadgets to get a probing security proof, and thus the randomness requirement for some secure shared circuits. We apply our method to a recent AES implementation secured with higher-order masking in bitslice and we show that we can save all the refresh gadgets involved in the s-box layer, which results in an significant performance gain.

2015

ASIACRYPT

#### Program Committees

- Crypto 2024
- CHES 2022 (Program chair)
- CHES 2022
- Asiacrypt 2022
- Eurocrypt 2022
- CHES 2021
- Asiacrypt 2021
- CHES 2020
- TCC 2020
- Asiacrypt 2020
- CHES 2019
- Asiacrypt 2019
- Asiacrypt 2018
- CHES 2018

#### Coauthors

- Michel Abdalla (1)
- Gilles Barthe (2)
- Fabrice Benhamouda (2)
- Gaëtan Cassiers (1)
- Jean-Sébastien Coron (2)
- Pierre-Evariste Dagand (1)
- François Dupressoir (1)
- Thomas Espitau (1)
- Pierre-Alain Fouque (5)
- Benoît Gérard (2)
- Dahmun Goudarzi (1)
- Benjamin Grégoire (1)
- Benjamin Grégoire (1)
- Jean-Gabriel Kammerer (1)
- Darius Mercadier (1)
- Alain Passelègue (2)
- Emmanuel Prouff (4)
- Matthieu Rivain (7)
- Mélissa Rossi (1)
- Pierre-Yves Strub (1)
- Abdul Rahman Taleb (4)
- Adrian Thillard (2)
- Mehdi Tibouchi (1)
- Serge Vaudenay (2)
- Damien Vergnaud (3)
- Raphaël Wintersdorff (1)