Implementation and Assessment of Strong Logic Encryption Techniques
Date
2021
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
The increasing cost of building, operating, managing, and maintaining state-of-the-art silicon manufacturing facilities has pushed several stages of the semiconductor device’s manufacturing supply chain offshore. However, many of these offshore facilities are identified as untrusted entities. Processing and fabrication of ICs in an untrusted supply chain pose a number of challenging security threats such as IC overproduction, Trojan insertion, Reverse Engineering, Intellectual Property (IP) theft, and counterfeiting. To counter these threats, various hardware design-for-trust techniques have been proposed. Logic obfuscation, as a proactive technique among these techniques, has been introduced as a technique that obfuscates and conceals the functionality of IC/IP using additional key inputs that are driven by an on-chip tamper-proof memory. Shortly after introducing the primitive logic locking solutions, a very strong attack based on the satisfiability solvers (SAT) was shown that could break all previously proposed locking mechanisms in almost polynomial time. To thwart this attack, researchers have investigated many directions, such as formulating locking solutions that significantly increase the number of required SAT iterations, or formulating the locking solutions such that it is not translatable to a SAT problem. However, further investigations demonstrated that some of these locking techniques are vulnerable to other types of attacks such as removal attacks, approximate attacks, bypass attack, and Satisfiability Module Theories (SMT) attack. Besides, these techniques suffer from very low output corruption. Hence, an inactivate IC behaves almost identical to an unlocked IC except one or a few inputs. For addressing these challenges, first, we will characterize the SAT attack, which shows that how using different SAT solvers can produce different results with large deviations which demonstrates that long execution time or high memory usage in one SAT solver may not be a problem in another solver. Next, we discuss a branch of SAT-resilient methods called cyclic locking and propose efficient methods to introduce feedbacks into a circuit in a way that SAT and its improved versions for cyclic circuits could not find the correct key. Then, we discuss a new branch of obfuscation techniques that tries to restrict access to the scan chain and thus circumvent the SAT attack. In there, we discuss a new attack method called unrolling SAT that potentially could be used for breaking obfuscated scan chains and recover the protected design. Last, we propose an open source framework that replaces SAT solvers with formal verification tools and could be used on a broader range of problems.