Improving Bounded Model Checkers Scalability for Circuit De-Obfuscation: An Exploration.

With the globalization and distribution of the semiconductor supply chain, intellectual property (IP) protection has become a necessity. Recent years have witnessed a surge of interest in logic locking as a proactive IP protection solution. However, in recent years, we also have seen an increase in logic/circuit de-obfuscation attacks that put the strength of logic locking at risk. One of these attacks on locked circuits is the bounded-model-checker (BMC)-based attack, where the adversary has limited access to the design-for-testability (DFT) (known as scan chain). While the BMC-based attack is widely known as an algorithmic attack, numerous studies show that the attack lacks scalability since it has two unrolling factors: sequential unrolling and miter duplication. Inspired by straightforward heuristics widely used for satisfiability problems in the computer science SAT community, in this paper, we will explore a set of methodologies that can have a significant impact on mitigating the BMC attack’s scalability issue. For this purpose, through the BMC attack process, we explore the efficacy of " restart " and " initialization " on the attack performance, in which we apply some modification on the locked design before (" initialization ") or within (" restart ") the BMC execution. By applying " restart " and " initialization " in numerous different configurations, our experimental results show > 85% consistent improvement in the BMC attack that can lead to a stronger algorithmic attack scenario on logic locking.