International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Sonia Belaïd

Affiliation: CryptoExperts, France

Publications

Year
Venue
Title
2020
EUROCRYPT
Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations 📺
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.
2018
EUROCRYPT
2018
ASIACRYPT
Tight Private Circuits: Achieving Probing Security with the Least Refreshing
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.
2017
CRYPTO
2016
EUROCRYPT
2016
ASIACRYPT
2015
EPRINT
2015
EPRINT
2015
EPRINT
2015
EPRINT
2015
EPRINT
2015
EUROCRYPT
2015
ASIACRYPT
2015
CHES
2014
EPRINT
2014
ASIACRYPT
2013
CHES

Program Committees

CHES 2020
CHES 2019
Asiacrypt 2019
CHES 2018
Asiacrypt 2018