Paper 2021/1468

LeakageVerif: Scalable and Efficient Leakage Verification in Symbolic Expressions

Quentin L. Meunier, Sorbonne University
Etienne Pons, Sorbonne University
Karine Heydemann, Sorbonne University
Abstract

Side-channel attacks are a powerful class of attacks targeting cryptographic devices. Masking is a popular protection technique to thwart such attacks as it can be theoretically proven secure. However, correctly implementing masking schemes is a non-trivial task and error-prone. If several techniques have been proposed to formally verify masked implementations, they all come with limitations regarding expressiveness, scalability or accuracy. In this work, we propose a symbolic approach, based on a variant of the classical substitution method, for formally verifying arithmetic and boolean masked programs. This approach is more accurate and scalable than existing approaches thanks to a careful design and implementation of key heuristics, algorithms and data structures involved in the verification process. We present all the details of this approach and the open-source tool called LeakageVerif which implements it as a python library, and which offers constructions for symbolic expressions and functions for their verification. We compare LeakageVerif to three existing state-of-the-art tools on a set of 46 masked programs, and we show that it has very good scalability and accuracy results while providing all the necessary constructs for describing algorithmic to assembly masking schemes. Finally, we also provide the set of 46 benchmarks, named MaskedVerifBenchs and written for comparing the different verification tools, in the hope that they will be useful to the community for future comparisons.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint.
Keywords
Implementation Side-Channel Attacks Masking Countermeasure Automated verification LeakageVerif
Contact author(s)
quentin meunier @ lip6 fr
etienne pons @ polytechnique edu
karine heydemann @ lip6 fr
History
2022-07-15: revised
2021-11-06: received
See all versions
Short URL
https://ia.cr/2021/1468
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2021/1468,
      author = {Quentin L.  Meunier and Etienne Pons and Karine Heydemann},
      title = {{LeakageVerif}: Scalable and Efficient Leakage Verification in Symbolic Expressions},
      howpublished = {Cryptology {ePrint} Archive, Paper 2021/1468},
      year = {2021},
      url = {https://eprint.iacr.org/2021/1468}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.