SAT-hard Cyclic Logic Obfuscation for Protecting the IP in the Manufacturing Supply Chain
This addresses the problem of protecting intellectual property in hardware manufacturing supply chains against reverse engineering, though it is incremental as it builds on existing cyclic obfuscation methods.
The paper tackles the vulnerability of cyclic logic obfuscation to SAT-based attacks by showing that missing cycle avoidance clauses can cause solver failures, and proposes techniques to exponentially increase cycles and attack complexity, making such attacks infeasible with exponential runtime growth.
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 pre-processing step and define various key combinations that could open or close cycles without making the circuit oscillating or stateful. In this paper, we show that this pre-processing 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 feedbacks. We further illustrate that when the number of feedbacks is increased, the pre-processing 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 pre-processing 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 paper is implemented, it would impose an exponentially difficult problem for the satisfiability solver based attacks.