Hardware Trojans refer to additional logic maliciously implanted by attackers in integrated circuits (ICs). Because of the potential security threat of hardware Trojans, they have attracted extensive attention to security issues. As a formal verification method, property checking has been proved to be a powerful solution for hardware Trojan detection. However, existing property-checking methods are limited by the unity of security properties and the model explosion problem of formal models. The limitations above hinder the practical applications of these methods. To alleviate these challenges, we propose an effective property-checking method for hardware Trojan detection. Specifically, we establish the formal model based on the principle of finite state machine (FSM), and the method can alleviate the model explosion problem. For property writing, we extract the core behavior characteristics of hardware Trojans and then generate properties for the verification of certain types of hardware Trojans. Experimental results demonstrate that our approach is applicable to detect information leakage and denial of service (DoS) hardware Trojans by verifying security properties.

Physical unclonable functions (PUFs) are emerging as highly promising lightweight hardware security primitives that offer novel information security solutions. PUFs capitalize on the intrinsic physical variations within circuits to generate unpredictable responses. Nevertheless, diverse PUF types often encounter difficulties in concurrently fulfilling multiple performance requisites. As is well known, strong PUFs possess significantly larger challenge–response pair (CRP) set sizes. However, they are vulnerable to machine learning (ML) attacks. Conversely, weak PUFs generate responses with superior randomness, yet their CRP sets are inadequate to satisfy the demands of practical applications. This paper presents a newly devised double-latch PUF (DL-PUF) to address this issue. This design significantly enhances both the CRP set size and security performance. The available CRPs of the DL-PUF design can reach up to $2^{64}$, and its robust security features are also demonstrated in this paper. We have implemented this design on twelve 45 nm Xilinx Spartan 6 XC6SLX25 FPGAs. The experimental results indicate that our proposed DL-PUF performs well in terms of reliability, uniqueness, uniformity, and randomness. Additionally, three machine learning algorithms were employed to conduct comprehensive tests on the DL-PUF. The results reveal its excellent resilience against machine learning attacks.

Electromagnetic side-channel analysis (EM SCA) attack poses a serious threat to integrated circuits (ICs), necessitating timely vulnerability detection before deployment to enhance EM side-channel security. Various EM simulation methods have emerged for analyzing EM side-channel leakage, providing sufficiently accurate results. However, these simulator-based methods still face two principal challenges in the design process of high security chips. Firstly, the large volume of measurement data required for a single security evaluation results in substantial time overhead. Secondly, design iterations lead to repetitive security evaluations, thus increasing the evaluation cost. In this paper, we propose EMSIM+ which includes two efficient and accurate layout-level EM side-channel leakage evaluation frameworks named EMSIM+GAN and EMSIM+GAN+TL to mitigate the above challenges, respectively. EMSIM+GAN integrates a Generative Adversarial Network (GAN) model that utilizes the chip’s cell current and power grid information to predict EM emanations quickly. EMSIM+GAN+TL further incorporates transfer learning (TL) within the framework, leveraging the experience of existing designs to reduce the training datasets for new designs and achieve the target accuracy. We compare the simulation results of EMSIM+ with the state-of-the-art EM simulation tool, EMSIM as well as silicon measurements. Experimental results not only prove the high efficiency and high simulation accuracy of EMSIM+, but also verify its generalization ability across different designs and technology nodes.

Hardware intellectual property (IP) cores from untrusted vendors are widely used, raising security concerns for system designers. Although formal methods provide powerful solutions for detecting malicious behaviors in hardware, the participation of manual work prevents the methods from reaching practical applications. For example, Information Flow Tracking (IFT) represents a powerful approach to preventing leakage of sensitive information. However, existing IFT solutions either introduce hardware overheads or lack practical automatic working procedures, especially for hardware sequential logic. To alleviate these challenges, we propose a framework that fully automates information leakage detection at the gate level of hardware. This framework introduces Z3, an SMT solver, to automatically check the violation of confidentiality. On the other hand, an automatic tool is developed to remove the manual workload further. In this tool, the gate level hardware is converted to the formal model firstly, and the integrity of the model is assessed. Along with the model converting step, the property for leakage detection is generated as well. The proposed solution is tested on 25 gate-level netlist benchmarks, where sequential designs are included to validate the effectiveness. As a result, Trojans leaking information from circuit outputs can be automatically detected. The measured time consumption of the entire working procedure validates the efficiency of the proposed approach.

To shorten the development cycle of integrated circuit (IC) chips, third-party IP cores (3PIPs) are widely used in the design phase; however, these 3PIPs may be untrusted, creating potential vulnerabilities. Attackers may insert hardware Trojans (HTs) into 3PIPs, resulting in the leakage of critical information, alteration of circuit functions, or even physical damage to circuits. This has attracted considerable attention, leading to increased research efforts focusing on detection methods for HTs. This paper proposes a K-Hypergraph model construction methodology oriented towards the abstraction of HT characteristics, aiming at detecting HTs. This method employs the K-nearest neighbors (K-NN) algorithm to construct a hypergraph model of gate-level netlists based on the extracted features. To ensure data balance, the SMOTE algorithm is employed before constructing the K-Hypergraph model. Then, the K-Hypergraph model is trained, and the weights of the K-Hypergraph are updated to accomplish the classification task of distinguishing between Trojan nodes and normal nodes. The experimental results demonstrate that, when evaluating Trust-Hub benchmark performance indicators, the proposed method has average balanced accuracy of 91.18% in classifying Trojan nodes, with a true positive rate (TPR) of 92.12%.

This paper analyzes the underlying logic of the processor’s behavior level code. It proposes an automatic model construction and formal verification method for the cache consistency protocol with the aim of ensuring data consistency in the processor and the correctness of the cache function. The main idea of this method is to analyze the register transfer level (RTL) code directly at the module level and variable level, and extract the key modules and key variables according to the code information. Then, based on key variables, conditional behavior statements are retrieved from the code, and unnecessary statements are deleted. The model construction and simplification of related core states are completed automatically, while also simultaneously generating the attribute library to be verified, using “white list” as the construction strategy. Finally, complete cache consistency protocol verification is implemented in the model detector UPPAAL. Ultimately, this mechanism reduces the 142 state-transition path-guided global states of the cache module to be verified into 4 core functional states driven by consistency protocol implementation, effectively reducing the complexity of the formal model, and extracting 32 verification attributes into 6 verification attributes, reducing the verification time cost by 76.19%.