Noé Amiot
Sorbonne Université, LIP6, CNRS, 4 Place Jussieu 75005, Paris, France

Quentin Meunier
Sorbonne Université, LIP6, CNRS, 4 Place Jussieu 75005, Paris, France

Karine Heydemann
Sorbonne Université, LIP6, CNRS, 4 Place Jussieu 75005, Paris, France; Thales, Meyreuil, France

Emmanuelle Encrenaz
Sorbonne Université, LIP6, CNRS, 4 Place Jussieu 75005, Paris, France

Keywords: Side-Channel Attacks, Masking, Micro-Architectural Leakage Detection, Formal Verification

Abstract

Verifying the security of masked hardware and software implementations, under advanced leakage models, remains a significant challenge, especially when accounting for glitches, transitions and CPU micro-architectural specifics. Existing verification approaches are either restricted to small hardware gadgets, small programs on CPUs such as Sboxes, limited leakage models, or require hardware-specific prior knowledge.In this work, we present aLEAKator, an open-source framework for the automated formal verification of masked cryptographic accelerators and software running on CPUs from their HDL descriptions. Our method introduces mixed-domain simulation, enabling precise modeling and verification under various (including robust and relaxed) 1-probing leakage models, and supports variable signal granularity without being restricted to 1-bit wires. aLEAKator also supports verification in the presence of lookup tables, and does not require prior knowledge of the target CPU architecture. Our approach is validated against existing tools and real-world measurements while providing innovative results such as the verification of a full, first-order masked AES on various CPUs.