NNgSAT：神经网络引导的逻辑锁定复杂结构SAT攻击
NNgSAT: Neural Network guided SAT Attack on Logic Locked Complex Structures
摘要：
集成电路供应链的全球化带来了许多安全威胁，特别是当涉及不可信方时。这就需要一种可靠的逻辑混淆解决方案来应对这些威胁。在2010年代的十年中，逻辑混淆的各种威胁和对策中，布尔可满足性（SAT）攻击或其衍生物之一可以打破几乎所有最先进的逻辑混淆对策。然而，在某些情况下，特别是当逻辑锁定电路包含复杂结构时，例如大乘法器、大路由网络或大树结构，逻辑锁定电路难以被SAT攻击解决。使用这些结构进行混淆可能会导致强大的防御，因为许多SAT求解器无法处理这种复杂性。然而，在本文中，我们提出了一个神经网络引导的SAT攻击（NNgSAT），在其中，我们研究的能力和有效性的消息传递神经网络（MPNN）解决这些复杂的结构（SAT硬实例）。在NNgSAT中，在被训练为分类器以预测SAT问题的SAT/UNSAT（NN用作SAT求解器）之后，神经网络用于指导/帮助实际SAT求解器找到SAT分配。通过在逻辑锁定电路数据集对应的合取范式（CNFs）上训练神经网络，并对神经网络预测的置信度进行微调，实验表明NNgSAT可以在合理的时间内解决93.5%的包含复杂结构的逻辑锁定电路，而现有的SAT攻击无法进行其中的攻击流程。
英文摘要：
The globalization of the IC supply chain has raised many security threats, especially when untrusted parties are involved. This has created a demand for a dependable logic obfuscation solution to combat these threats. Amongst a wide range of threats and countermeasures on logic obfuscation in the 2010s decade, the Boolean satisfiability (SAT) attack, or one of its derivatives, could break almost all state-of-the-art logic obfuscation countermeasures. However, in some cases, particularly when the logic locked circuits contain complex structures, such as big multipliers, large routing networks, or big tree structures, the logic locked circuit is hard-to-be-solved for the SAT attack. Usage of these structures for obfuscation may lead a strong defense, as many SAT solvers fail to handle such complexity. However, in this paper, we propose a neural-network-guided SAT attack (NNgSAT), in which we examine the capability and effectiveness of a message-passing neural network (MPNN) for solving these complex structures (SAT-hard instances). In NNgSAT, after being trained as a classifier to predict SAT/UNSAT on a SAT problem (NN serves as a SAT solver), the neural network is used to guide/help the actual SAT solver for finding the SAT assignment(s). By training NN on conjunctive normal forms (CNFs) corresponded to a dataset of logic locked circuits, as well as fine-tuning the confidence rate of the NN prediction, our experiments show that NNgSAT could solve 93.5% of the logic locked circuits containing complex structures within a reasonable time, while the existing SAT attack cannot proceed the attack flow in them.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
