Efficiency analysis of SAT solvers in logic locking applications

• Main Author: Liu, Zhiyuan
• Other Authors: Gwee Bah Hwee
• Format: Final Year Project
• Language: English
• Published: Nanyang Technological University 2024
• Subjects: Engineering
• Online Access: https://hdl.handle.net/10356/177292
• Institution: Nanyang Technological University

As globalization affects integrated circuit (IC) design, logic locking has emerged as an important protective strategy against numerous security threats. Since the introduction of the SAT attack method, the reliability of logic locking has been questioned. This development has spurred further research into SAT attacks and their effects on logic lock defenses. However, the literature currently lacks a comparative analysis of the efficiency of different SAT solvers. This report begins by reviewing the essential concepts of logic lock circuits, the basics of hardware attacks, and how SAT solvers operate. This foundation helps to understand how each solver performs in real-world scenarios. It then explores SAT attacks in more depth, applying these concepts through specific attack algorithms in practice. For the experimental setup, the high-performance NVIDIA RTX A5000 was chosen as the hardware base, and the Python programming language was used to develop the experimental environment, ensuring the experiments were both effective and precise. Experimental results show that the Cadical153 solver exhibits excellent performance when observing and processing logic in a single clause due to its innovative local search strategy. In addition, compared with other solvers, Cadical153 showed the highest efficiency in multiple test scenarios. By analyzing the root causes of these performance differences, it also provides valuable guidance for the design and improvement of encryption circuits. Most importantly, this report highlights the importance of analyzing the efficiency of SAT solvers and provides specific suggestions for future research directions. This research not only fills the existing research gap, but also provides experimental basis and theoretical support for technological progress in the field of IC design.