By: Rakibul Hassan (George Mason University), Gaurav Kohle (UC Davis), Setareh Rafatirad (UC Davis), Houman Homayoun (UC Davis), and Sai Manoj Pudukotai Dinakarrao (George Mason University)
Stage: Gate-Level
Summary
We propose a neural network-based cognitive SAT to SAT-hard clause translator under the constraints of minimal PPA overheads while preserving the original functionality with impenetrable security. Our proposed method is incubated with a SAT-hard clause generator that translates the existing conjunctive normal form (CNF) through minimal perturbations such as inclusion of pair of inverters or buffers or adding new lightweight SAT-hard block depending on the provided CNF. For efficient SAT-hard clause generation, the proposed method 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. For a fair comparison with the state-of-the-art, we evaluate our proposed technique on ISCAS’85 and ISCAS’89 benchmarks. It is seen to successfully defend against multiple state-of-the-art SAT attacks devised for hardware RE with minimal overheads.
Contact
Input/Output Interface
- Input: ISCAS’85 Bench File
- Output: Obfuscated Netlist
Dependencies
MiniSAT SAT solver
References
Learning a SAT Solver from Single-Bit Supervision Journal Article
In: CoRR, vol. abs/1802.03685, 2018.