Fun-SAT

This repo contains the source code for Functional Corruptibility-Guided SAT-Based Attack on Sequential Logic Encryption.

For more information about the tool, please visit our HOST'21 paper.

Tool Dependency:

The tool has been successfully tested on Ubuntu 18.04.5 LTS and CentOS Stream 8.

Python 3.6 or higher version
nuXmv (Please put the absolute path of the tool executable to src/nuxmv_config.txt)
VCS (Please put the absolute path of the tool executable to src/vcs_config.txt)
Modified version of the SAT attack tool originally developed by Pramod Subramanyan and Sayak Ray (After compiling this tool, please put the executable sld to src/)
All the tool dependencies required by the above tools.

Netlist Format:

Must be Verilog files with the file suffix of .v.
Must be synchronous active high reset.
Currently, the tool only supports two-input gates, inverters, buffers, and posedge Flip-Flops (with the name of DFF_*) from the Nangate Open Cell library.
The names of the clock signal and the reset signal should be clk and reset, respectively.

Please make sure the format of your netlists is the same as that of the sample netlists in sample_run/ folder.

Command Format:

python unroll_sat.py <original netlist> 
                     <encrypted netlist> 
                     <key length> 
                     <bounded time window size>
                     <FC difference threshold>
                     <FC hold threshold> 
                     <Simulation count> 
                     <Time-out in seconds> 
                     <Fun-SAT enable (1 or 0)>

Note when the Fun-SAT feature is not enabled, i.e., the last argument is 0, all Fun-SAT-related arguments will not be used. However, the user should still put some arbitrary values as the placeholder.

Sample Command (with the Fun-SAT feature):

python unroll_sat.py ./sample_run/s27_ori.v ./sample_run/s27_kl4_uc10.v 4 50 0.01 5 1000 100000 1

Sample Output:


Original netlist: ./sample_run/s27_ori.v
Encrypted netlist: ./sample_run/s27_kl4_uc10.v
Key length in cycle count: 4
Original netlist: Verilog to Bench finished.
Encrypted netlist: Verilog to Bench finished.
Original netlist: Sequential to Combinational finished.
Encrypted netlist: Sequential to Combinational finished.

********** FC analysis phase ************

Simulating... (Unroll_count=1) 0.0
Simulating... (Unroll_count=2) 0.121
Simulating... (Unroll_count=3) 0.232
Simulating... (Unroll_count=4) 0.36
Simulating... (Unroll_count=5) 0.43
Simulating... (Unroll_count=6) 0.565
Simulating... (Unroll_count=7) 0.679
Simulating... (Unroll_count=8) 0.776
Simulating... (Unroll_count=9) 0.893
Simulating... (Unroll_count=10) 1.0
Simulating... (Unroll_count=11) 1.0
Simulating... (Unroll_count=12) 1.0
Simulating... (Unroll_count=13) 1.0
Simulating... (Unroll_count=14) 1.0
Simulating... (Unroll_count=15) 1.0

********** SAT attack phase *************

Feasible unroll cycles: 11
#DIPs = 2
Key prediction: 1001100101111100
Unique key passed!
key=1001100101111100

********** Attack Summary ***************

TotalRuntime: 46.11986494064331 sec.
Runtime (Attack): 45.779550552368164 sec.
UC:1, BMC:0, UMC:0
Succeeded at unroll cycles b=11
key=1001100101111100

Cite our work:

Please cite our work if you find this codebase useful to you:

@inproceedings{hu2021fun,
  title={{Fun-SAT}: Functional Corruptibility-Guided {SAT}-Based Attack on Sequential Logic Encryption},
  author={Hu, Yinghua and Zhang, Yuke and Yang, Kaixin and Chen, Dake and Beerel, Peter A and Nuzzo, Pierluigi},
  booktitle={International Symposium on Hardware Oriented Security and Trust (HOST)},
  pages={281--291},
  year={2021},
  organization={IEEE}
}