Benchmarking SAT Solvers in Hardware Security and Their GPU Acceleration

Abstract

The recent trend in the Integrated Circuit (IC) supply chain process involves, in-house development and out-sourcing the designs to major fabrication labs located globally. This process introduces several concerns and threats like Intellectual Property (IP) piracy, reverse engineering, IC counterfeiting and introduction of hardware Trojans. An awareness of these attacks and threats have led to the introduction of several hardware-level security techniques. This thesis comprises a review of the Hardware-level security techniques on Logic Locking, their strength against the Boolean Satisfiability solvers and an attempt to parallelize the SAT-Solver on a GPU, which is at the core of the de-obfuscation tool used for the security analysis. We investigate the strength of six different SAT solvers in attacking various obfuscation schemes. Our investigation revealed that Glucose and Lingeling SAT solvers are generally suited for attacking small-to-midsize obfuscated circuits, while xii MapleGlucose, if the system is not memory bound, is best suited for attacking mid-to-difficult obfuscation methods. The GPU version of the SAT-Solver was implemented using the NVIDIA’s CUDA toolkit, as to take advantage of the hundreds/thousands of CUDA cores present on the GPUs. However, the results of GPU parallelization are not as promising as one would think in the general sense, and the drawbacks of the approach are also reported clearly. The results of the GPU based SAT Solver are derived using the benchmarks available in the SATLIB website.