INDIANA - Verifying (Random) Probing Security through Indistinguishability Analysis

Despite masking being a prevalent protection against passive side-channel attacks, implementing it securely in hardware remains a manual, challenging, and error-prone process. This paper introduces INDIANA, a comprehensive security verification tool for hardware masking. It provides a hardware verification framework, enabling a complete analysis of simulation-based security in the glitch-extended probing model, with cycle-accurate estimations for leakage probabilities in the random probing model. Notably, INDIANA is the first framework to analyze arbitrary masked circuits in both models, even at the scale of full SPN cipher rounds (e.g., AES), while delivering exact verification results. To attain precise and extensive verifiability, we introduce a partitionable probing distinguisher that enables rapid verification of probe tuples, outperforming state-of-the-art methods based on statistical independence. Most interestingly, our approach inherently facilitates extensions to the random probing model by leveraging Fast Fourier-Hadamard Transformations (FFTs). Benchmark results show that INDIANA competes effectively with leading probing model verification tools, such as maskVerif and VERICA. Notably, INDIANA the first tool that is capable to provide cycle-accurate estimations of random probing leakage probabilities for large-scale masked circuits.