International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations

Authors:
Sonia Belaïd , CryptoExperts, Paris, France
Pierre-Evariste Dagand , Sorbonne Université, Paris, France
Darius Mercadier , Sorbonne Université, Paris, France
Matthieu Rivain , CryptoExperts, Paris, France
Raphaël Wintersdorff
Download:
DOI: 10.1007/978-3-030-45727-3_11 (login may be required)
Search ePrint
Search Google
Conference: EUROCRYPT 2020
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.
Video from EUROCRYPT 2020
BibTeX
@inproceedings{eurocrypt-2020-30256,
  title={Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations},
  booktitle={39th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Zagreb, Croatia, May 10–14, 2020, Proceedings},
  series={Lecture Notes in Computer Science},
  publisher={Springer},
  keywords={Compiler;Masking;Automated verification;Bitslice},
  volume={12105},
  doi={10.1007/978-3-030-45727-3_11},
  author={Sonia Belaïd and Pierre-Evariste Dagand and Darius Mercadier and Matthieu Rivain and Raphaël Wintersdorff},
  year=2020
}