On the Security of Sequential Logic Locking Against Oracle-Guided Attacks
Yinghua Hu, Yuke Zhang, Kaixin Yang, Dake Chen, Peter A. Beerel, Pierluigi Nuzzo · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2023
The Boolean satisfiability (SAT) attack is an oracle-guided attack that can break most combinational logic locking schemes by efficiently pruning out all the wrong keys from the search space. Extending such an attack to sequential logic locking requires multiple time-consuming rounds of SAT solving, performed using an “unrolled” version of the sequential circuit, and model checking, used to determine the successful termination of the attack. This article addresses these challenges by formally characterizing the relation between the minimum unrolling depth required to prune out the wrong keys of an SAT-based attack and a notion of functional corruptibility (FC) for sequential circuits, which can be efficiently estimated from a locked circuit to indicate the progress of an SAT-based attack. Based on this analysis, we present an FC-guided SAT-based attack that can significantly reduce unnecessary SAT and model-checking tasks. We present two versions of the attack, namely,Fun-SATandFun-SAT+, based on whether the attacker has a priori knowledge of the key length.Fun-SATaims to find the correct key sequence, whileFun-SAT+aims to retrieve the correct initial state of the circuit. The numerical evaluation shows thatFun-SATcan be, on average,$90\boldsymbol {\times }$faster than previous attacks against state-of-the-art locking methods. On the other hand, when using an approximate termination condition,Fun-SAT+can find an initial state that leads to at most 0.1% FC in 76.9% instances that would otherwise time out after one day.