Armand Schinkel
Ruhr University Bochum, Bochum, Germany

Pascal Sasdrich
Ruhr University Bochum, Bochum, Germany

Keywords: Side-Channel Analysis, Fault Injection Analysis, Combined Analysis, formal verification, leakage function, Fourier-Hadamard Transform

Abstract

Cryptographic hardware implementations are vulnerable to combined physical implementation attacks, integrating Side-Channel Analysis (SCA) and Fault Injection Analysis (FIA) to compromise their security. Although theoretically sound countermeasures exist, their practical application is often complicated and error-prone, making automated security verification a necessity. Various tools have been developed to address this need, using different approaches to formally verify security, but they are limited in their ability to analyze complex hardware circuits in the context of Combined Analysis (CA) and advanced probabilistic adversary models.In this work, we introduce a novel verification method that assesses the security of complex hardware circuits in the context of random probing with random faults, a scenario that more closely reflects real-world combined attack scenarios. Our approach centers around symbolic fault simulation and the derivation of a fault-enhanced leakage function using the Fourier-Hadamard Transform (FHT), enabling the computation of tight leakage probabilities for arbitrary circuits and providing a more accurate and comprehensive security analysis. By integrating our method into the INDIANA security verification framework, we extended its capabilities to analyze the leakage behavior of circuits in the presence of random faults, demonstrating the practicality of our approach.The results of our evaluation highlight the versatility and scalability of our approach, which can efficiently compute leakage probabilities under various fault scenarios for large-scale attacks, e. g., for a masked round of the PRESENT cipher. Notably, our method can complete most experiments in less than an hour, demonstrating a significant improvement over existing estimation-based tools. This achievement confirms the potential of our approach to provide a more comprehensive and practically useful security assessment of hardware circuits, and marks an important step forward for the development of secure hardware systems.