Paper 2017/1227

VerMI: Verification Tool for Masked Implementations

Victor Arribas, Svetla Nikova, and Vincent Rijmen

Abstract

Masking is a widely used countermeasure against Side-Channel Attacks (SCA), but the implementation of these countermeasures is challenging. Experimental security evaluation requires special equipment, a considerable amount of time and extensive technical knowledge. So, to automate and to speed up this process, a formal verification can be performed to asses the security of a design. Multiple theoretical approaches and verification tools have been proposed in the literature. The majority of them are tailored for software implementations, not applicable to hardware since they do not take into account glitches. Existing hardware verification tools are limited either to combinational logic or to small designs due to the computational resources needed. In this work we present VerMI, a verification tool in the form of a logic simulator that checks the properties defined in Threshold Implementations to address the security of a hardware implementation for meaningful orders of security. The tool is designed so that any masking scheme can be evaluated. It accepts combinational and sequential logic and is able to analyze an entire cipher in short time. With the tool we have managed to spot a flaw in the round-based Keccak implementation by Gross et al., published in DSD 2017.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint. MAJOR revision.
Keywords
VerMIMaskingFormal VerificationNon-completenessUniformityGlitchesLogic Simulator
Contact author(s)
varribas @ esat kuleuven be
Svetla Nikova @ esat kuleuven be
vincent rijmen @ esat kuleuven be
History
2017-12-22: received
Short URL
https://ia.cr/2017/1227
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/1227,
      author = {Victor Arribas and Svetla Nikova and Vincent Rijmen},
      title = {{VerMI}: Verification Tool for Masked Implementations},
      howpublished = {Cryptology {ePrint} Archive, Paper 2017/1227},
      year = {2017},
      url = {https://eprint.iacr.org/2017/1227}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.