Armistice: Micro-Architectural Leakage Modelling for Masked Software Formal Verification

Arnaud de Grandmaison; Karine Heydemann; Quentin L.  Meunier

Paper 2022/467

Armistice: Micro-Architectural Leakage Modelling for Masked Software Formal Verification

Arnaud de Grandmaison

Karine Heydemann, Sorbonne University

Quentin L. Meunier

, Sorbonne University

Abstract

Side channel attacks are powerful attacks for retrieving secret data by exploiting physical measurements such as power consumption or electromagnetic emissions. Masking is a popular countermeasure as it can be proven secure against an attacker model. In practice, software masked implementations suffer from a security reduction due to a mismatch between the considered leakage sources in the security proof and the real ones, which depend on the micro-architecture. We present the model of a system comprising an Arm Cortex-M3 obtained from its RTL description and test-vectors, as well as a model of the memory of a STM32F1 board, built exclusively using test-vectors. Based on these models, we propose Armistice, a framework for formally verifying the absence of leakage in first-order masked implementations taking into account the modelled micro-architectural sources of leakage. We show that Armistice enables to pinpoint vulnerable instructions in real world masked implementations and helps design masked software implementations which are practically secure.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint.
Keywords: Side Channel Attacks Masking Verification Micro-architectural Leakage
Contact author(s): Arnaud DeGrandmaison @ arm com
karine heydemann @ lip6 fr
quentin meunier @ lip6 fr
History: 2022-07-13: revised; 2022-04-22: received; See all versions
Short URL: https://ia.cr/2022/467
License: CC BY

BibTeX

@misc{cryptoeprint:2022/467,
      author = {Arnaud de Grandmaison and Karine Heydemann and Quentin L.  Meunier},
      title = {Armistice: Micro-Architectural Leakage Modelling for Masked Software Formal Verification},
      howpublished = {Cryptology ePrint Archive, Paper 2022/467},
      year = {2022},
      note = {\url{https://eprint.iacr.org/2022/467}},
      url = {https://eprint.iacr.org/2022/467}
}