Transactions on Cryptographic Hardware and Embedded Systems 2025
A TRAP for SAT:
On the Imperviousness of a Transistor-Level Programmable Fabric to Satisfiability-Based Attacks
README
TRANSAT
TRANSAT, or "Transistor-Level SAT Tools", is a Python library for launching SAT-related functions on digital circuits implemented on the transistor level.
These functions include SAT attacks and SAT-based verification. These tools can be extended to other types of logic circuits, including logic-locked circuits.
Installation
Use the package manager pip to install a locally-downloaded TRANSAT distribution (available from dist/), or contact
Aric for the package. Icarus Verilog (iVerilog) may be installed easily using apt.
sudo apt install iverilog python3-pip
git clone https://github.com/aric-fowler/TRANSAT
cd TRANSAT/dist/
pip3 install *.tar.gz # Alternatively: $ pip3 install *.whl
To use the ABC SAT attack, download ABC and install it using the included Makefile, along with the TRANSAT package.
Usage
Command Terminal (Recommended):
# Help & run description:
satAttack -h
satVerify -h
stateLocate -h
# User manual:
man satAttack
man satVerify
# Basic SAT attack:
satAttack <plLogicFile> <ioCSV> <oracleNetlist> <oracleName> [-z]
# Basic SAT verification:
satVerify <plEncryptedFile> <plFunctionFile> <ioCSV> <keyValueCSV>
# Alternative SAT attack based on ABC tool:
abcAttack <encryptedVerilog> <oracleVerilog>
# State location in propositional netlists:
stateLocate <plLogicFile> <ioCSV>
For examples on how to run a SAT attack, see the shell scripts in the test/ directory. The output of a SAT attack is "extracted_key.csv", located in the work/
directory created by the attack script. Verification tool results are printed directly to the terminal.
Within Python:
# SAT attack:
from transat import satAttack
satAttack(plLogicFile,inputList,keyList,outputList,oracleNetlist,oracleName)