SRCLock: SAT-Resistant Cyclic Logic Locking for Protecting the Hardware
This addresses hardware security for chip designers by making it harder to reverse-engineer or tamper with integrated circuits, though it appears incremental as it builds on existing cyclic obfuscation methods.
The paper tackles the problem of hardware security by proposing SRCLock, a cyclic logic locking method that resists SAT attacks by exponentially increasing the complexity of CycSAT's pre-processing step, preventing correct key extraction in reasonable time.
In this paper, we claim that cyclic obfuscation, when properly implemented, poses exponential complexity on SAT or CycSAT attack. The CycSAT, in order to generate the necessary cycle avoidance clauses, uses a pre-processing step. We show that this pre-processing step has to compose its cycle avoidance condition on all cycles in a netlist, otherwise, a missing cycle could trap the SAT solver in an infinite loop or force it to return an incorrect key. Then, we propose several techniques by which the number of cycles is exponentially increased with respect to the number of inserted feedbacks. We further illustrate that when the number of feedbacks is increased, the pre-processing step of CycSAT faces an exponential increase in complexity and runtime, preventing the correct composition of loop avoidance clauses in a reasonable time before invoking the SAT solver. On the other hand, if the pre-processing is not completed properly, the SAT solver will get stuck or return incorrect key. Hence, when the cyclic obfuscation in accordance to the conditions proposed in this paper is implemented, it would impose an exponential complexity with respect to the number of inserted feedback, even when the CycSAT solution is used.