By: Yinghua Hu (University of Southern California), Yuke Zhang (University of Southern California), Kaixin Yang (University of Southern California), Dake Chen (University of Southern California), Peter A. Beerel (University of Southern California), and Pierluigi Nuzzo (University of Southern California)
Fun-SAT is a Boolean satisfiability (SAT)-based attack against sequential logic locking. Fun-SAT relies on a notion of functional corruptibility for a sequential circuit to efficiently estimate the minimum unrolling depth required for a successful SAT attack to prune out of the search space all the wrong keys of a locked circuit. Therefore, in a SAT-based attack to sequential logic locking, Fun-SAT can significantly reduce both the SAT-attack effort spent to produce candidate keys and the model checking effort spent to prove that a set of candidate keys is correct. The attack can effectively be used to evaluate the security of sequential locking schemes.
- Input: Gate-level netlist of the locked circuit, oracle access to the original circuit, and cycle length of the key sequence
- Output: Correct key sequence
Python 3.6 or higher version
Synopsys VCS (https://www.synopsys.com/verification/simulation/vcs.html)
SAT attack tool (https://github.com/descyphy/Modified_SAT_Attack_on_Logic_Locking)
In: 2021 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), IEEE, 2021.
- This work was supported in part by the Air Force Research Laboratory (AFRL) and the Defense Advanced Research Projects Agency (DARPA) under agreement number FA8650-18-1-7817.