Home
This repository contains RANE, the research platform which was created at George Mason University's GATE Lab to investigate the use of formal verification tools for logic locking deobfuscation.
The source code is released under a BSD-3-Clause license as basis for further research.
This tool includes Python modules needed to implement the so-called SAT attack on combinational and sequential circuits. The combinational attack is based on the paper proposed by late Pramod Subramanyan and has the following algorithm:
El Massad proposed an extension to this attack for sequential circuits that requires creating a combinational equivalent of the sequential circuit and unrolling until one of the termination criteria met:
This package includes multiple modules to parse gate level netlists in bench and verilog format and to implement these
two attacks using two different interfaces using formal verification tools or directly using SAT solvers. Here is an
overview of the available modules and files in this package:
This interface uses Pyverilog to generate verilog modules to carry out the deobfuscation attack. These verilog modules include SVA assumptions and assertions needed to find the desirable distinguishing inputs for the attack. This interface, then, feeds these files to a formal verification tool to find a counterexample with desired values.
Currently, this interface supports SymbiYosys and Cadence JasperGold. One major feature of this interface is that it could accept any valid Verilog input, including designs with multiple Verilog files and designs with hierarchies and complex blocks. Also, by using formal verification tools, unrolling of the sequential circuit happens implicitly inside the tool, which simplifies the attack implementation with much more flexibility.
Our main audience for developing this interface was hardware security research community. By using this tool it is possible to implement and insert any logic locking structure/modification in high-level Verilog/SystemVerilog in a Verilog circuit and evaluate it directly without any synthesis or structure simplification. This could provide researchers with much higher flexibility and easier access to an evaluation platform.
Details of this interface and its usage is available in Formal Tool Interface page.
This interface uses pySMT to implement Seq/SAT attack. Similar to the original SAT attack developed by Subramanyan, this interface applies Tseitin transformation on gate level elements and supports only the primitive NOT/AND/NAND/OR/NOR/XOR/XNOR gates. Details of this interface is available in SAT Interface page.
Obfuscated and original circuits/designs needed to be parsed prior to the attack. Two parsers are provided for bench and
Verilog formats that could read the necessary port definitions and if needed, the complete structure of the circuit for
gate level netlists. Pyverilog could also be used for parsing purposes, but it is slow for large circuits.
In some cases, like detecting cycles in a netlist, we need to apply graph-related algorithms on the equivalent directed cyclic graph (DCG) of the circuit. RANE includes a translator that parses a netlist and ports it into a graph data structure in NetworkX. NetworkX includes most of the useful graph algorithms and its output could be used in the attack process or for obfuscation purposes.
ISCAS'85, ISCAS'89, and MCNC circuits are provided in the benchmarks folder. These benchmarks are available
in .bench
and .v format. For more information on the benchmark circuits check Benchmarks page.
NEOS: Closed-source tool developed by University of Florida for comb/seq attack.
SLD: Original tool developed by Subramanyan for SAT attack.
CircuitGraph: Tools for working with circuits as graphs in Python by CMU.
Design-for-Excellence Lab: Github of research team in NYU Abu Dhabi.
HAL: A comprehensive netlist reverse engineering and manipulation framework by Ruhr University.
We have used the following packages for developing RANE:
SymbiYosys: Formal verification tool
Pyverilog: Verilog parser, analyzer, generator
pySMT: Provide a SAT independent interface to SAT solvers
NetworkX: Graph processing