The issue of securing microchip designs against hardware attacks has grown in magnitude as more and more embedded systems are deployed in hostile environments, where security measures have to be taken to prevent attackers from accessing unwanted information.
The first step in solving this problem is gaining awareness of the security vulnerabilities in a design, which can be done through a fault injection campaign. Current solutions tackle the issue by either requiring silicon manufacturing for every prototype, which is expensive, or simulating faults using a model of the device under test and of the possible faults being injected, which takes a considerable amount of time. Some hybrid solutions have been developed to improve this aspect (namely, by using FPGAs to implement the device and injecting faults on it instead), but they still require some form of specialized hardware to operate.
Moreover, a gap still remains between the results from these tools and the work necessary to update the design and mitigate the vulnerabiliies found. Results usually reference cells in the netlist, while the development is mostly done in a high-level hardware descriptive language.
This thesis proposes two improvements to the currently existing workflow: first, it explores the effectiveness of equivalence checking in tracing individual gates in the netlist representation back to the RTL lines that generated them, and second, it builds on the simulation-based fault injection approach by introducing a formal framework to prove the presence or absence of successful faults.
The results show that equivalence checking can significantly increase the number of cells recognized as results of individual RTL lines of code, enabling a designer to better pinpoint which components should be hardened against fault injection attacks. In terms of fault identification, the framework described can reduce the number of faults to be simulated down to 2% of the number necessary to exhaustively check a design for possible vulnerabilities, greatly speeding up existing simulation-based approaches.