skip to main content
Explore Scholarly Publications and Datasets in the NSF-PAR

Title: NNgSAT: Neural Network guided SAT Attack on Logic Locked Complex Structures
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 more » 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. « less
Authors:
Award ID(s):
1718434 2200446
Publication Date:
NSF-PAR ID:
10298702
Journal Name:
2020 IEEE/ACM International Conference On Computer Aided Design (ICCAD)
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; ( , IACR transactions on cryptographic hardware and embedded systems)
    In this paper, we introduce the Satisfiability Modulo Theory (SMT) attack on obfuscated circuits. The proposed attack is the superset of Satisfiability (SAT) attack, with many additional features. It uses one or more theory solvers in addition to its internal SAT solver. For this reason, it is capable of modeling far more complex behaviors and could formulate much stronger attacks. In this paper, we illustrate that the use of theory solvers enables the SMT to carry attacks that are not possible by SAT formulated attacks. As an example of its capabilities, we use the SMT attack to break a recent obfuscation scheme that uses key values to alter delay properties (setup and hold time) of a circuit to remain SAT hard. Considering that the logic delay is not a Boolean logical property, the targeted obfuscation mechanism is not breakable by a SAT attack. However, in this paper, we illustrate that the proposed SMT attack, by deploying a simple graph theory solver, can model and break this obfuscation scheme in few minutes. We describe how the SMT attack could be used in one of four different attack modes: (1) We explain how SMT attack could be reduced to a SAT attack,more »(2) how the SMT attack could be carried out in Eager, and (3) Lazy approach, and finally (4) we introduce the Accelerated SMT (AccSMT) attack that offers significant speed-up to SAT attack. Additionally, we explain how AccSMT attack could be used as an approximate attack when facing SMT-Hard obfuscation schemes.« less
  2. ; ; ; ( , IACR transactions on cryptographic hardware and embedded systems)
    In this paper, we introduce the Satisfiability Modulo Theory (SMT) attack on obfuscated circuits. The proposed attack is the superset of Satisfiability (SAT) attack, with many additional features. It uses one or more theory solvers in addition to its internal SAT solver. For this reason, it is capable of modeling far more complex behaviors and could formulate much stronger attacks. In this paper, we illustrate that the use of theory solvers enables the SMT to carry attacks that are not possible by SAT formulated attacks. As an example of its capabilities, we use the SMT attack to break a recent obfuscation scheme that uses key values to alter delay properties (setup and hold time) of a circuit to remain SAT hard. Considering that the logic delay is not a Boolean logical property, the targeted obfuscation mechanism is not breakable by a SAT attack. However, in this paper, we illustrate that the proposed SMT attack, by deploying a simple graph theory solver, can model and break this obfuscation scheme in few minutes. We describe how the SMT attack could be used in one of four different attack modes:(1) We explain how SMT attack could be reduced to a SAT attack,(2) howmore »the SMT attack could be carried out in Eager, and (3) Lazy approach, and finally (4) we introduce the Accelerated SMT (AccSMT) attack that offers significant speed-up to SAT attack. Additionally, we explain how AccSMT attack could be used as an approximate attack when facing SMT-Hard obfuscation schemes.« less
  3. ; ; ; ( , Proceedings of the 2021 on Great Lakes Symposium on VLSI)
    To enable trust in the IC supply chain, logic locking as an IP protection technique received significant attention in recent years. Over the years, by utilizing Boolean satisfiability (SAT) solver and its derivations, many de-obfuscation attacks have undermined the security of logic locking. Nonetheless, all these attacks receive the inputs (locked circuits) in a very simplified format (Bench or remapped and translated Verilog) with many limitations. This raises the bar for the usage of the existing attacks for modeling and assessing new logic locking techniques, forcing the designers to undergo many troublesome translations and simplifications. This paper introduces the RANE Attack, an open-source CAD-based toolbox for evaluating the security of logic locking mechanisms that implement a unique interface to use formal verification tools without a need for any translation or simplification. The RANE attack not only performs better compared to the existing de-obfuscation attacks, but it can also receive the library-dependent logic-locked circuits with no limitation in written, elaborated, or synthesized standard HDL, such as Verilog. We evaluated the capability/performance of RANE on FOUR case studies, one is the first de-obfuscation attack model on FSM locking solutions (e.g., HARPOON) in which the key is not a static bit-vector but amore »sequence of input patterns.« less
  4. ; ; ; ( , 22nd International Symposium on Quality Electronic Design (ISQED))
    null (Ed.)
    Logic locking has been widely evaluated as a proactive countermeasure against the hardware security threats within the IC supply chain. However, the introduction of the SAT attack, and many of its derivatives, has raised big concern about this form of countermeasure. In this paper, we explore the possibility of exploiting chaos computing as a new means of logic locking. We introduce the concept of chaotic logic locking, called ChaoLock, in which, by leveraging asymmetric inputs in digital chaotic Boolean gates, we define the concept of programmability (key-configurability) to the sets of underlying initial conditions and system parameters. These initial conditions and system parameters determine the operation (functionality) of each digital chaotic Boolean gate. Also, by proposing dummy inputs in chaotic Boolean gates, we show that during reverse-engineering, the dummy inputs conceal the main functionality of the chaotic Boolean gates, which make the reverse-engineering almost impossible. By performing a security analysis of ChaoLock, we show that with no restriction on conventional CMOS-based ASIC implementation and with no test/debug compromising, none of the state-of-the-art attacks on logic locking, including the SAT attack, could reformulate chaotic Boolean gates while dummy inputs are involved and their parameters are locked. Our analysis and experimental resultsmore »show that with a low number of chaotic Boolean gates mixed with CMOS digital gates, ChaoLock can guarantee resiliency against the state-of-the-art attacks on logic locking at low overhead.« less
  5. ; ; ; ; ( , IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems)
    Protecting intellectual property (IP) has become a serious challenge for chip designers. Most countermeasures are tailored for CMOS integration and tend to incur excessive overheads, resulting from additional circuitry or device-level modifications. On the other hand, power density is a critical concern for sub-50 nm nodes, necessitating alternate design concepts. Although initially tailored for error-tolerant applications, imprecise computing has gained traction as a general-purpose design technique. Emerging devices are currently being explored to implement ultra-low-power circuits for inexact computing applications. In this paper, we quantify the security threats of imprecise computing using emerging devices. More specifically, we leverage the innate polymorphism and tunable stochastic behavior of spin-orbit torque (SOT) devices, particularly, the giant spin-Hall effect (GSHE) switch. We enable IP protection (by means of logic locking and camouflaging) simultaneously for deterministic and probabilistic computing, directly at the GSHE device level. We conduct a comprehensive security analysis using state-of-the-art Boolean satisfiability (SAT) attacks; this study demonstrates the superior resilience of our GSHE primitive when tailored for deterministic computing. We also demonstrate how probabilistic computing can thwart most, if not all, existing SAT attacks. Based on this finding, we propose an attack scheme called probabilistic SAT (PSAT) which can bypass the defensemore »offered by logic locking and camouflaging for imprecise computing schemes. Further, we illustrate how careful application of our GSHE primitive can remain secure even on the application of the PSAT attack. Finally, we also discuss side-channel attacks and invasive monitoring, which are arguably even more concerning threats than SAT attacks.« less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email