The SAT Attack

This chapter elaborates on the SAT attack, which breaks all pre-SAT logic locking techniques. The SAT attack is an oracle-guided attack that utilizes a SAT solver to compute attack patterns that refine the key search space iteratively. The SAT attack has changed the direction of logic locking research; developing efficient countermeasures against the attack is still an active area of research. This chapter presents the SAT attack, which breaks all pre-SAT logic locking techniques. The SAT attack forms the most potent variant of key recovery attacks mounted to break basic combinational logic locking techniques [10]. The attack and its variants apply to both logic locking [10] and camouflaging [4, 5]. The attack uses the notion of Boolean satisfiability. Section 4.1 reviews the fundamental concepts of Boolean satisfiability. Section 4.2 presents the SAT attack algorithm. Section 4.3 elaborates on the effectiveness of the SAT attack against the pre-SAT logic locking techniques. Section 4.4 discusses the potential approaches to thwart the SAT attack. Section 4.5 presents a formal security analysis framework to quantify security of logic locking techniques against different classes of attacks including the SAT attack.