SRCLock: SAT-Resistant Cyclic Logic Locking for Protecting the Hardware

TL;DR

This paper introduces SRCLock, a cyclic obfuscation technique that significantly increases the complexity of SAT-based attacks by exponentially increasing the number of cycles and feedbacks, making the attack computationally infeasible.

Contribution

The paper proposes novel cyclic obfuscation methods that exponentially increase cycle counts, thereby thwarting SAT and CycSAT attacks effectively.

Findings

Cyclic obfuscation can exponentially increase attack complexity.

Proper implementation of cycle avoidance clauses is crucial for security.

The proposed techniques prevent CycSAT from efficiently generating key solutions.

Abstract

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.