Paper 2017/897

Formal Verification of Masked Hardware Implementations in the Presence of Glitches

Roderick Bloem, Hannes Gross, Rinat Iusupov, Bettina Könighofer, Stefan Mangard, and Johannes Winter

Abstract

Masking provides a high level of resistance against side-channel analysis. However, in practice there are many possible pitfalls when masking schemes are applied, and implementation flaws are easily overlooked. Over the recent years, the formal verification of masked software implementations has made substantial progress. In contrast to software implementations, hardware implementations are inherently susceptible to glitches. Therefore, the same methods tailored for software implementations are not readily applicable. In this work, we introduce a method to formally verify the security of masked hardware implementations that takes glitches into account. Our approach does not require any intermediate modeling steps of the targeted implementation and is not bound to a certain leakage model. The verification is performed directly on the circuit’s netlist, and covers also higher-order and multivariate flaws. Therefore, a sound but conservative estimation of the Fourier coefficients of each gate in the netlist is calculated, which characterize statistical dependence of the gates on the inputs and thus allow to predict possible leakages. In contrast to existing practical evaluations, like t-tests, this formal verification approach makes security statements beyond specific measurement methods, the number of evaluated leakage traces, and the evaluated devices. Furthermore, flaws detected by the verifier are automatically localized. We have implemented our method on the basis of an SMT solver and demonstrate the suitability on a range of correctly and incorrectly protected circuits of different masking schemes and for different protection orders. Our verifier is efficient enough to prove the security of a full masked AES S-box, and of the Keccak S-box up to the third protection order.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published by the IACR in EUROCRYPT 2018
Keywords
maskingformal verificationthreshold implementationshardware securityside-channel analysisprivate circuits
Contact author(s)
hannes gross @ iaik tugraz at
History
2018-02-01: last of 3 revisions
2017-09-24: received
See all versions
Short URL
https://ia.cr/2017/897
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/897,
      author = {Roderick Bloem and Hannes Gross and Rinat Iusupov and Bettina Könighofer and Stefan Mangard and Johannes Winter},
      title = {Formal Verification of Masked Hardware Implementations in the Presence of Glitches},
      howpublished = {Cryptology ePrint Archive, Paper 2017/897},
      year = {2017},
      note = {\url{https://eprint.iacr.org/2017/897}},
      url = {https://eprint.iacr.org/2017/897}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.