International Association
for Cryptologic Research

Modern system-on-chip (SoC) designs are becoming prone to numerous security threats due to their critical applications and ever-growing complexity and size. Therefore, the early stage of the design flow requires comprehensive security verification. The control flow of an SoC, generally implemented using finite state machines (FSMs), is not an exception to this requirement. Any deviations from the desired flow of FSMs can cause serious security issues. On the other hand, the control FSMs may be prone to fault-injection and denial-of-service (DoS) attacks or have inherent information leakage and access control issues at the gate-level netlist abstraction. Therefore, defining a set of security rules (guidelines) for obtaining FSM implementations free from particular security vulnerabilities after performing logic synthesis is crucial. Unfortunately, as of today, no solution exists in the state-of-the-art domain to verify the security of control FSMs. In this paper, we propose a set of such security rules for control FSM design and a verification framework called ARC-FSM-G to check for those security rule violations at pre-silicon to prevent any security vulnerabilities of FSM against fault-injection, access control, and information leakage threats. Experimental results on several benchmarks varying in size and complexity illustrate that ARC-FSM-G can effectively check for violations of all the proposed rules within a few seconds.