Paper 2023/732

VerifMSI: Practical Verification of Hardware and Software Masking Schemes Implementations

Quentin L. Meunier, Sorbonne University
Abdul Rahman Taleb
Abstract

Side-Channel Attacks are powerful attacks which can recover secret information in a cryptographic device by analysing physical quantities such as power consumption. Masking is a common countermeasure to these attacks which can be applied in software and hardware, and consists in splitting the secrets in several parts. Masking schemes and their implementations are often not trivial, and require the use of automated tools to check for their correctness. In this work, we propose a new practical tool named VerifMSI which extends an existing verification tool called LeakageVerif targeting software schemes. Compared to LeakageVerif, VerifMSI includes hardware constructs, namely gates and registers, what allows to take glitch propagation into account. Moreover, it includes a new representation of the inputs, making it possible to verify three existing security properties (Non-Interference, Strong Non-Interference, Probe Isolating Non-Interference) as well as a newly defined one called Relaxed Non-Interference, compared to the unique Threshold Probing Security verified in LeakageVerif. Finally, optimisations have been integrated in VerifMSI in order to speed up the verification. We evaluate VerifMSI on a set of 9 benchmarks from the literature, focusing on the hardware descriptions, and show that it performs well both in terms of accuracy and scalability.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint.
Keywords
Side-Channel AttacksMasking VerificationThreshold Probing SecurityNon-Interference
Contact author(s)
quentin meunier @ lip6 fr
History
2023-05-25: approved
2023-05-22: received
See all versions
Short URL
https://ia.cr/2023/732
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2023/732,
      author = {Quentin L. Meunier and Abdul Rahman Taleb},
      title = {VerifMSI: Practical Verification of Hardware and Software Masking Schemes Implementations},
      howpublished = {Cryptology ePrint Archive, Paper 2023/732},
      year = {2023},
      note = {\url{https://eprint.iacr.org/2023/732}},
      url = {https://eprint.iacr.org/2023/732}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.