Formal verification of processor microarchitecture to analyze system security against fault attacks

From bibtex.

Abstract

Fault injection attacks are a serious threat to system security, enabling attackers to bypass protection mechanisms or access sensitive information. While the security of these systems is traditionally assessed at the software or hardware level, recent research highlights the need to consider both and analyze the processor microarchitecture to fully understand the consequences of fault attacks. In this context, this thesis introduces an exhaustive and automated analysis technique, comprising both software and hardware system descriptions, to better understand the final consequences of hardware-level faults on software and provide formal guarantees of software security. For this purpose, we propose microArchiFI, a formal modeling and verification methodology to evaluate fault effects on combined hardware/software systems. Built on top of the Yosys compiler, this tool generates a system model suitable for formal verification techniques such as bounded model checking. Unlike previous methodologies, microArchiFI is exhaustive and allows for automatic identification of corner-case vulnerabilities, as well as proving system robustness against fault attacks. We validate our methodology on RISC-V processors by automatically identifying known fault attacks exploiting microarchitectural mechanisms.