You are looking at a specific version 20150527:192221 of this paper. See the latest version.

Paper 2015/506

Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler

Gilles Barthe and Sonia Belaïd and François Dupressoir and Pierre-Alain Fouque and Benjamin Grégoire

Abstract

The prevailing approach for building masked algorithms that can resist higher-order differential power analysis is to develop gadgets, that is, masked gates used as atomic blocks, that securely implement basic operations from the original algorithm, and then to compose these gadgets, introducing refresh operations at strategic places to guarantee that the complete circuit is protected. These compositional principles are embedded in so-called masking transformations, which are used as heuristics to achieve secure composition. Unfortunately, these transformations are seldom proved secure rigorously, and in fact, sometimes yield algorithms that are not secure against higher-order attacks. In this paper, we define a notion of strong simulatability that naturally supports compositional principles. Although this notion is stronger than the notion of simulatability (or perfect simulation) from previous works, we show that it is satisfied by several gadgets from the literature, including the mask refreshing gadget from Duc, Dziembowski and Faust (Eurocrypt 2014), the secure multiplication gadget from Rivain and Prouff (CHES 2010) and the secure multiplication gadget between dependent inputs from Coron et al. (FSE 2013). Then, we exploit a tight connection between strong simulatability and probabilistic information flow policies to define a (fine-grained, incremental) type system that checks (strong) simulatability of algorithms. We use the type system to validate a novel and automated transformation that outputs masked algorithms at arbitrary orders. Finally, we measure the performance of masked algorithms of AES, Keccak-f, Simon, and Speck generated by our transformation. The results are encouraging: for AES, masking at order 5, 20, and 100 respectively incur slowdowns of 100x, 750x, and x1500 w.r.t. the unmasked implementation given as input to our tool.

Metadata
Available format(s)
PDF
Category
Secret-key cryptography
Publication info
Preprint. MINOR revision.
Keywords
MaskingCompositionFormal MethodsCompilerType System
Contact author(s)
sonia belaid @ live fr
History
2016-10-25: revised
2015-05-27: received
See all versions
Short URL
https://ia.cr/2015/506
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.