On the Security of Sequential Logic Locking Against Oracle-Guided Attacks

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-SAT and Fun-SAT+, based on whether the attacker has a priori knowledge of the key length. Fun-SAT aims to find the correct key sequence, while Fun-SAT+ aims to retrieve the correct initial state of the circuit. The numerical evaluation shows that Fun-SAT can be, on average, 90x 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.