ARMISTICE: Microarchitectural Leakage Modeling for Masked Software Formal Verification - Sorbonne Université
Journal Articles IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems Year : 2022

ARMISTICE: Microarchitectural Leakage Modeling for Masked Software Formal Verification

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 propose ARMISTICE, a framework for formally verifying the absence of leakage in first-order masked implementations taking into account modelled micro-architectural sources of leakage. As a proof of concept, we present the modelling of an Arm Cortex-M3 core from its RTL description and leakage test vectors, as well as the modelling of the memory of a STM32F1 board, exclusively using leakage test vectors. We show that, with these models, ARMISTICE pinpoints vulnerable instructions in real world masked implementations and helps the design of masked software implementations which are practically secure.
Fichier principal
Vignette du fichier
armistice_hal.pdf (750.33 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Licence

Dates and versions

hal-03954892 , version 1 (24-01-2023)

Licence

Identifiers

Cite

Arnaud De Grandmaison, Karine Heydemann, Quentin L. Meunier. ARMISTICE: Microarchitectural Leakage Modeling for Masked Software Formal Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022, 41 (11), pp.3733-3744. ⟨10.1109/TCAD.2022.3197507⟩. ⟨hal-03954892⟩
73 View
97 Download

Altmetric

Share

More