By: Shervin Roshanisefat (George Mason University) and Avesta Sasan (George Mason University)
Stage: RTL, HDL
Summary
This package is a collection of pluggable functions and classes in Python for assessing obfuscated circuits. These components include:
- A SAT interface using pySMT to easily interface with different SAT solvers
- A formal verification tool interface to use SystemVerilog for SAT queries
- A graph interface to NetworkX and graph-tools libraries for graph processing
- Verilog and bench format IO read/write functions
The toolkit has several modules out-of-the box using the available components:
- Combinational SAT attack code in less than 250 lines of Python.
- An unrolling SAT attack implementation using the SAT interface.
- An unrolling SAT attack implementation using formal verification tool interface configured for Symbiyosys. This module accepts high-level Verilog or SystemVerilog code and treats it as an obfuscated or oracle circuit.
- Implementations of several obfuscation techniques.
Implemented modules have comparable performance with the available SAT attack binaries implemented in C since SAT calls are handled using binary files.
Contact
Input/Output Interface
- Input: Verilog and Bench files
- Output: Key information
Dependencies
- Python
- Symbiyosys
- pySMT
Licensing Info
BSD 3-clause