SAT-Hard Cyclic Logic Obfuscation for Protecting the IP in the Manufacturing Supply Chain

摘要

State-of-the-art attacks against cyclic logic obfuscation use satisfiability solvers that are equipped with a set of cycle-avoidance clauses. These cycle-avoidance clauses are generated in a preprocessing step and define various key combinations that could open or close cycles without making the circuit oscillating or stateful. In this article, we show that this preprocessing step has to generate cycle-avoidance conditions on all cycles in a netlist; otherwise, a missing cycle could trap the solver in an infinite loop or make it exit with an incorrect key. Then, we propose several techniques by which the number of cycles is exponentially increased as a function of the number of inserted feedback. We further illustrate that when the number of feedback is increased, the preprocessing step of the attack faces an exponential increase in complexity and runtime, preventing the correct composition of cycle-avoidance clauses in a reasonable time. On the other hand, if the preprocessing is not concluded, the attack formulated by the satisfiability solver will either get stuck or exit with an incorrect key. Hence, when the cyclic obfuscation under the conditions proposed in this article is implemented, it would impose an exponentially difficult problem for the satisfiability solver-based attacks.