Quality Assessment of RFET-based Logic Locking Protection Mechanisms using Formal Methods

The high distribution of the manufacturing of Integrated Circuits (ICs) over different foundries yields long and untrustworthy supply chains. Logic locking is one prominent protection technique against malicious usage and counterfeit. The emerging technology of Reconfigurable Field-Effect Transistors (RFETs) has recently been utilized to implement new polymorphic logic mechanisms to protect intellectual property. The mechanisms’ assessment is important to reinforce the newly introduced protection mechanism and, hence, avoid any weak logic structures. So far, approximate Hamming Distance-based assessment techniques have been used for determining the protection quality while considering combinatorial circuits only. This work proposes a novel method to assess the quality of the RFET-based logic locking structures for sequential circuits. In particular, formal techniques are orchestrated to analyze the circuit’s state space to determine whether any incorrect keys exist that unintentionally unlock and exhibit the circuit’s correct functional behavior. The experimental evaluation validates that the proposed scheme unveils weaknesses of the protection structure, which remain undetected when using existing techniques.