Paper 2016/590

Mitigating SAT Attack on Logic Locking

Yang Xie and Ankur Srivastava

Abstract

Logic locking is a technique that has been proposed to protect outsourced IC designs from piracy and counterfeiting by untrusted foundries. It can hide the functionality of an IC by inserting key-controlled logic gates into the original design. The locked IC preserves the correct functionality only when a correct key is provided. Recently, the security of logic locking is threatened by a new type of attack called satisfiability checking (SAT) based attack, which can decipher the correct key of most logic locking techniques within a few hours [11] even for reasonably large number of keys. This type of attack iteratively solves SAT formulas which progressively eliminate the incorrect keys till the circuit unlocked. In this paper, we present a specially designed circuit block (referred to as Anti-SAT block) to thwart the SAT attack. We show that the number of SAT attack iterations to reveal the correct key in a circuit comprising an Anti-SAT block is an exponential function of the key-size thereby making the SAT attack computationally infeasible. This is a substantial result because a) we illustrate how to construct the functionality of the Anti- SAT block and b) using a mathematically rigorous approach to prove that if chosen correctly, the Anti-SAT block makes SAT attack computationally infeasible (exponential in key-size). Moreover, through our experiments, we illustrate the effectiveness of our approach to securing modern chips fabricated in untrusted foundries.