Case Study: Fault-Injection Vulnerability Assessment at RTL Level

The increasing complexity and global distribution of hardware design processes present significant security challenges to embedded devices. Among these challenges, fault injection attacks stand out as severe physical threats that can alter the control flow of a device. These attacks compromise the integrity, confidentiality, and availability of the device by tampering with critical locations. Therefore, analyzing the fault injection vulnerability of a circuit is crucial for understanding the general effects of faults and identifying potential countermeasures. However, most research in this area focuses on the gate-level or layout-level analysis. While this approach is representative of fabricated designs, it does not allow for the early detection of vulnerabilities and the application of necessary mitigation strategies. This paper introduces a formal methodology to assess fault injection vulnerabilities at the Register-Transfer Level (RTL). Our approach leverages formal verification techniques to systematically introduce faults into the RTL representation of hardware components, taking into account design-specific security properties. This method facilitates the identification and analysis of potential security weaknesses. We demonstrate the effectiveness of this methodology by applying it to industry-standard hardware IP cores. Our experimental results underscore the importance of incorporating formal fault injection techniques early in the hardware development lifecycle. By performing early preemptive vulnerability assessments, system integrity can be enhanced significantly.