Impact of Satisfiability Solvers on Logic Locking

The use of logic locking is becoming an essential technique to secure microelectronic products against unauthorized and malicious actions, such as IP piracy and IC overproduction. However, as the IC supply chain flow has evolved and becomes more advanced and more complex, adversaries have been able to exploit algorithms, tools, devices, and other resources to undermine the effectiveness of DfTr solutions. With no exception, logic locking has also faced numerous attacks that have shown the need for increasingly sophisticated countermeasures. One particularly potent attack on logic locking comes from the use of Boolean satisfiability solvers, which were already used widely for implementation optimization, testing, and verification. This chapter aims to provide a detailed account of this type of attack, including both satisfiability-based and algorithm-based methods. By examining the assumptions made in the threat model described in Chap. 5 (Sect. 5.3.2 ), readers will gain insight into the specifics of such attacks, and with the ongoing evolution of the IC supply chain flow and the emergence of new threats, it is crucial that designers remain vigilant and proactive in developing robust countermeasures to protect their designs.