A Neural Network-based SAT-Resilient Obfuscation Towards Enhanced Logic Locking

• URL: http://arxiv.org/abs/2209.05799v1
• Date: Tue, 13 Sep 2022 07:59:27 GMT
• Title: A Neural Network-based SAT-Resilient Obfuscation Towards Enhanced Logic Locking
• Authors: Rakibul Hassan, Gaurav Kolhe, Setareh Rafatirad, Houman Homayoun, Sai Manoj Pudukotai Dinakarrao
• Abstract summary: We propose a neural network-based unSAT clause translator, SATConda. SATConda incurs a minimal area and power overhead while preserving the original functionality with impenetrable security. Our proposed SATConda is evaluated on ISCAS85 and ISCAS89 benchmarks.
• Score: 3.076761061950216
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Logic obfuscation is introduced as a pivotal defense against multiple hardware threats on Integrated Circuits (ICs), including reverse engineering (RE) and intellectual property (IP) theft. The effectiveness of logic obfuscation is challenged by the recently introduced Boolean satisfiability (SAT) attack and its variants. A plethora of countermeasures has also been proposed to thwart the SAT attack. Irrespective of the implemented defense against SAT attacks, large power, performance, and area overheads are indispensable. In contrast, we propose a cognitive solution: a neural network-based unSAT clause translator, SATConda, that incurs a minimal area and power overhead while preserving the original functionality with impenetrable security. SATConda is incubated with an unSAT clause generator that translates the existing conjunctive normal form (CNF) through minimal perturbations such as the inclusion of pair of inverters or buffers or adding a new lightweight unSAT block depending on the provided CNF. For efficient unSAT clause generation, SATConda is equipped with a multi-layer neural network that first learns the dependencies of features (literals and clauses), followed by a long-short-term-memory (LSTM) network to validate and backpropagate the SAT-hardness for better learning and translation. Our proposed SATConda is evaluated on ISCAS85 and ISCAS89 benchmarks and is seen to defend against multiple state-of-the-art successfully SAT attacks devised for hardware RE. In addition, we also evaluate our proposed SATCondas empirical performance against MiniSAT, Lingeling and Glucose SAT solvers that form the base for numerous existing deobfuscation SAT attacks.

Related papers

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
  arXiv  Detail & Related papers  (2024-10-18T22:25:54Z)
• Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
  We introduce CausalSAT, which employs causal reasoning to gain insights into the functioning of modern SAT solvers. We use CausalSAT to quantitatively verify hypotheses previously regarded as "rules of thumb" or empirical findings.
  arXiv  Detail & Related papers  (2023-06-09T22:53:16Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems. The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
  arXiv  Detail & Related papers  (2023-06-07T12:19:22Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  This paper introduces SATformer, a Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%.
  arXiv  Detail & Related papers  (2022-09-02T11:17:39Z)
• DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
  We present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem. DeepSAT achieves significant accuracy improvements over state-of-the-art learning-based SAT solutions.
  arXiv  Detail & Related papers  (2022-05-27T03:20:42Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• Learning Emergent Random Access Protocol for LEO Satellite Networks [51.575090080749554]
  We propose a novel grant-free random access solution for LEO SAT networks, dubbed emergent random access channel protocol (eRACH) eRACH is a model-free approach that emerges through interaction with the non-stationary network environment. Compared to RACH, we show from various simulations that our proposed eRACH yields 54.6% higher average network throughput.
  arXiv  Detail & Related papers  (2021-12-03T07:44:45Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Enhancing SAT solvers with glue variable predictions [2.635832975589208]
  We modify the state-of-the-art SAT solver CaDiCaL, improving its performance on SATCOMP 2018 and SATRACE 2019 with supervised learning and its performance on a dataset of SHA-1 preimage attacks with reinforcement learning. We address all these limitations, using a simpler network architecture allowing CPU inference for even large industrial problems with millions of clauses, and training instead to predict em glue variables---a target for which it is easier to generate labelled data, and which can also be formulated as a reinforcement learning task.
  arXiv  Detail & Related papers  (2020-07-06T07:16:49Z)
• Smooth Adversarial Training [120.44430400607483]
  It is commonly believed that networks cannot be both accurate and robust. Here we present evidence to challenge these common beliefs by a careful study about adversarial training. We propose smooth adversarial training (SAT), in which we replace ReLU with its smooth approximations to strengthen adversarial training.
  arXiv  Detail & Related papers  (2020-06-25T16:34:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.