KC2: Key-Condition Crunching for Fast Sequential Circuit Deobfuscation
Kaveh Shamsi1,a, Meng Li2,c, David Z. Pan2,d and Yier Jin1,b
1Department of Electrical and Computer Engineering, University of Florida
akshamsi@ufl.edu
byier.jin@ece.ufl.edu
2Department of Electrical and Computer Engineering, University of Texas at Austin
cmeng li@utexas.edu
ddpan@ece.utexas.edu
ABSTRACT
Logic locking and IC camouflaging are two promising techniques for thwarting an array of supply chain threats. Logic locking can hide the design from the foundry as well as end-users and IC camouflaging can thwart IC reverse engineering by end-users. Oracle-guided SAT-based deobfuscation attacks against these schemes have made it more and more difficult to securely implement them with low overhead. Almost all of the literature on SAT attacks is focused on combinational circuits. A recent first implementation of oracle-guided attacks on sequential circuits showed a drastic increase in deobfuscation time versus combinational circuits. In this paper we show that integrating the sequential SAT-attack with incremental boundedmodel-checking, and dynamic simplification of key-conditions (Key-Condition Crunching or KC2), we are able to reduce the runtime of sequential SAT-attacks by two orders of magnitude across benchmark circuits, significantly reducing the gap between sequential and combinational deobfuscation. These techniques are applicable to combinational deobfuscation as well and thus represent a generic improvement to deobfuscation procedures and help better understand the complexity of deobfuscation for designing secure locking/camouflaging schemes.