Logic locking is an effective approach for protecting integrated circuits against security threats such as Intellectual Property (IP) piracy and malicious design modifications. To defeat SAT attacks, state-of-the-art locking schemes, which are typically constructed using point-function that remains constant when the correct key is applied, while producing a wrong output only under a specific input pattern if an incorrect key is provided. Although this significantly increases the effort required for SAT attack, it introduces a new vulnerability that can be exploited to discover SAT-resilient blocks. Our observation is that pointfunction can lead to control signals, which exhibit significantly lower switching probability and yield clues for identifying anti-SAT cones. This work aims to reveal such clues at the level of FPGA netlist, where switching behavior characteristics can be quantified using the initialization vectors of Look-up-Tables (LUTs). We leverage the switching behavior measurements of LUTs to pinpoint signals with extremely low switching activity to locate control signals associated with SAT-resilient blocks. By forcing the identified control signals to a constant value, the protective function of the SAT-resilient blocks can be neutralized. We validate our attack method on locked circuits with anti-SAT enhancement. Experimental results on six compound logic locking schemes yield an average attack success rate of 99.6% and 100% key recovery rate for each neutralized circuit.

Fault attacks are effective side-channel attack methods for cryptanalysis. However, existing fault attack methods involve manual derivation of complex fault models or computation-intensive statistical analysis of mass faulty ciphertexts to recover the key. In addition, most methods are only applicable to a specific cryptographic algorithm with strict requirements on the type and quantity of faults injected, lacking scalability and generality. Taking inspiration from machine learning and formal verification, we propose an automated fault attack framework, which supports multi-byte fault attacks on both SPN and generalized Feistel structure ciphers. This framework automates the generation of formal fault propagation models, extraction of fault properties, and formal fault analysis. We construct formal fault propagation models for cipher designs to measure the fault propagation precisely, eliminating the requirement of manually deriving fault propagation models. We mine accurate invariable behaviors in fault propagation effects as fault properties using a small number of fault traces and further utilize property constraints to retrieve the key through formal analysis. This method implements a formal fault attack on SM4 in 25th to 28th rounds for the first time. Experimental results on AES, RSM, LED and SM4 demonstrate the effectiveness of our method, with key search complexity lower than or equal to state-of-the-art methods, while requiring only four faulty ciphertexts to recover a round key.

Model-based diagnosis (MBD) with multiple observations is complicated and difficult to manage over. In this paper, we proposed two new diagnosis models, namely, the Compacted Model with Multiple Observations (CMMO) and the Dominated-based Compacted Model with Multiple Observations (D-CMMO), to solve the problem in which a considerable amount of time is needed when multiple observations are given and more than one fault is injected. Three ideas are presented in this paper. First, we propose to encode MBD with each observation as a subsystem and share as many system variables as possible to compress the size of encoded clauses. Second, we utilize the notion of gate dominance in the CMMO approach to compute Top-Level Diagnosis with Compacted Model (CM-TLD) to reduce the solution space. Finally, we explore the performance of our model using three fault models. Experimental results on the ISCAS-85 benchmarks show that CMMO and D-CMMO perform better than the state-of-the-art algorithms.