aLEAKator: HDL Mixed-Domain Simulation for Masked Hardware \& Software Formal Verification

TL;DR

aLEAKator is an open-source framework that enables automated formal verification of masked cryptographic hardware and software, supporting complex leakage models and variable signal granularity without prior architecture knowledge.

Contribution

It introduces mixed-domain simulation for precise leakage modeling and verification, handling complex hardware/software features and realistic leakage scenarios.

Findings

Verified a full masked AES on various CPUs.

Supported complex leakage models including robust and relaxed.

Validated against existing tools and real-world measurements.

Abstract

Verifying the security of masked hardware and software implementations, under advanced leakage models, remains a significant challenge, especially then 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