Third-party intellectual property cores are essential building blocks of modern digital hardware. However, they usually come from vendors of different trust levels and may contain undocumented design functionality. Distinguishing such stealthy malicious design modifications remains a significant research challenge. State-of-the-art hardware Trojan detection methods usually require expert knowledge, sophisticated tools or large volumes of training samples. In this work, we make a step towards design for assurance by developing a Trojan detection method targeting look-up-table (LUT) netlists, which exploits the rich explicit structural and behavior characteristics embedded in the initialization vectors of LUTs to pinpoint Trojans. The proposed method automatically extracts a small set of high-quality Trojan related properties and detects Trojans through formal verification of the extracted properties, eliminating the limitation of manual property specification while covering a much wider range of Trojan designs. We further present a defense solution to mitigate the identified Trojans through lightweight design reconfiguration to neutralize the Trojan payload. The proposed method can be seamlessly integrated into the standard EDA flow to enable security to be evaluated along with functional correctness and performance budgets. Experimental results have demonstrated that our method can detect and mitigateTrust-Hub,ATTRITIONas well as satisfiability don't care Trojans.

The rapid evolution of unmanned aerial vehicles (UAVs) has positioned air-ground networks as vital infrastructures for diverse applications. However, the open channels of air-ground networks remain inherently vulnerable to persistent eavesdropping threats. While physical-layer key generation (PLKG) offers a lightweight security mechanism by leveraging channel reciprocity to extract shared secrets, the inherent mobility of UAVs introduces a paradoxical tradeoff. Increased channel randomness from dynamic flight patterns enhances security through entropy amplification but simultaneously disrupts channel reciprocity, leading to key mismatch between legitimate parties. Existing PLKG schemes struggle to maintain reliability in key generation due to static channel characteristics and synchronization overhead, limiting their practical deployment in air-ground networks. To resolve this conflict, we propose a Doppler shift key generation (DSKG) scheme that systematically regulates Doppler shifts through UAV trajectory design to derive secure keys. By formulating the problem as a Markov decision process, we develop a proximal policy optimization (PPO)-clip-based reinforcement learning algorithm to dynamically control UAV speed and steering angle, ensuring robust Doppler shift reciprocity while maximizing both key entropy and generation rate. Experimental results quantify the improvements of our scheme over benchmarks in maintaining high key unpredictability and generation efficiency. Furthermore, the analysis provides valuable insights into parameter impacts, confirming the practical viability of the DSKG scheme for securing air-ground communications.

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.

Trojans represent a severe threat to hardware security and trust. This work investigates the Trojan detection problem from a unique viewpoint and proposes a novel hardware Trojan localization method targeting FPGA netlists. The proposed method automatically extracts the rich structural and behavioral features at look-up-table (LUT) level to train an explainable graph neural network (GNN) model for classifying design nodes in FPGA netlists and identifying the Trojan-infected ones. Experimental results using 183 hardware Trojan benchmarks show that our method successfully pinpoints Trojan-infected nodes with true positive rate, accuracy and area under the ROC curve (AUC) of 95.14%, 95.71% and 95.46% respectively. To the best of our knowledge, this is the first LUT level Trojan localization solution using explainable GNNs.

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.

Large infrastructure networks play a crucial role in modern society, supporting various aspects of our daily lives. Reliability of such networks is a pivotal research conundrum, which has attracted intensive research interests in recent years. However, most of them focus on protecting critical nodes or optimizing the network topology through linear models to measure reliability, while nonlinear models for improving network reliability are rarely investigated. The major challenges are the significant computational complexity and damage to the original network structure caused by nonlinear methods. Inspired by the similarity in dynamics between heat conduction systems and infrastructure networks, we propose a nonlinear model that maps an infrastructure network to a nonlinear heat conduction system for the purpose of measuring and enhancing network reliability. We introduce a new evaluating indicator of network reliability based on community irrelevance. Additionally, we propose a new Edge Addition (EA) method called Modularity Addition (MA) that maximizes network reliability by adding multiple edges during each iteration and substantially reduces computational overhead. Experimental results have demonstrated that our MA method outperforms existing algorithms. Specifically, in comparison to the widely used EA and Posteriorly Adding (PA) algorithms, the proposed MA method improves network reliability by up to 13.2%. It reduces the number of edges added to the network by 72%. Moreover, the MA method offers a 6.8-fold reduction in time complexity compared to existing methods, highlighting its efficiency and scalability. Our approach is validated on both synthetic and real-world networks, showcasing its significant value on enhancing the robustness of complex infrastructure systems.

As the core engine of modern communication systems, digital circuits are encountering significant security risks of cyber-attacks. Hardware information flow tracking (IFT) is a powerful tool for integrated circuit design security verification and vulnerability detection. While there are a large body of hardware IFT methods at different levels of abstraction, look-up-table (LUT) level IFT is still an open research challenge due to the huge number of possible LUT configurations that all correspond to varying IFT behaviors. In this work, we make the first move towards LUT level IFT for field programmable gate array (FPGA) design security verification. Specifically, we design an algorithm that enables automatic creation of the precise IFT model for an arbitrary LUT and the generation of fine-grained IFT logic for FPGA netlists. Through using the generated IFT logic as the security model, we can formally prove security properties and hunt for security vulnerabilities. Experimental results have demonstrated that our method can detect the timing channels and hardware Trojans residing in the synthesized FPGA netlists of Trust-Hub benchmarks. Our work complements the spectrum of hardware security verification solutions at both the FPGA netlist and bitstream ends, which fills in the gap of post-synthesis FPGA design security verification tools.

Spatio-temporal query services have been playing an increasingly important role in people’s daily lives. While outsourcing such services to third parties (e.g., cloud servers) offers considerable benefits, it raises data privacy issues. However, no existing work can fully support secure and efficient spatio-temporal queries in outsourcing environments. In this paper, we investigate the problem of Spatio-Temporal Range queries over Encrypted databases (STRE). Firstly, we design a new index structure, called Hilbert Hierarchical Prefix Bloom tree (H2PB-tree), which reduces the search complexity of spatio-temporal range query to sublinear. Then, we build an efficient STRE construction called E-STRE in the single-cloud model based on H2PB-tree and symmetric hidden-vector encryption. Moreover, we perform sufficient security analysis and experimental test, and the results show E-STRE outperforms prior arts in terms of performance while guaranteeing data security. Compared with the prior arts presented under the single-cloud model, our construction reduces the query delay by at least 18×.

Hardware Trojans are malicious design modifications, which pose severe threats to hardware security and trust. Since integrated circuit (IC) designs are difficult to modify after chip fabrication, it is of great importance to detect Trojans in the early design stage. In this work, we propose a novel hardware Trojan detection method at register transfer level (RTL) through semantic feature extraction and natural language processing (NLP). We convert the hardware design to control and data flow graph (CDFG) and develop a depth-first search and sliding window based algorithm for extracting and segmenting paths. This process preserves the structural and semantic features of RTL code. We then employ the NLP technique to perform Trojan detection at the granularity of RTL code statement. Specifically, we train the FastText model, which is proficient in word representation and text classification, to precisely pinpoint the Trojan-infected statements. We further integrate the word bigram features during the training process to improve the Trojan detection performance. Experimental evaluations using Trust-Hub benchmarks show that the proposed method can successfully pinpoint hardware Trojans with true positive rate (TPR), true negative rate (TNR), accuracy and F1-score of 97.77%, 99.95%, 98.86% and 97.46% respectively on average.

Hardware Trojans (HTs) have emerged as a security threat to the integrated circuits (ICs) industry. To counteract this threat, various detection methods have been proposed, among which conventional machine learning (ML)-based techniques using heuristic features from gate-level netlists have gained wide acceptance. However, these methods are notably sensitive to minor perturbations in modifications of the test circuits, often resulting in decreased detection capabilities. Furthermore, the black-box nature of the ML models obscures the basis for their decisions. This lack of transparency makes it difficult to scrutinize and address potential flaws in the models, thereby further reducing the credibility of Trojan detection results. In response to these challenges, we propose a targeted solution that leverages the SHapley Additive exPlanations method (SHAP), which dismantles the black-box paradigm and clarifies the fundamental reasons behind the failure of existing detection methods under circuit sample perturbations. Building on these insights, we abandon classical ML-based detection in favor of a scheme based on graph learning (GL), which significantly reduces the average drop in Recall from 52.35% to 7.29% compared with the traditional method. Comparative experiments demonstrate that our proposed GL-based method effectively resolves the sensitivity issue related to the sample perturbations in existing HT detection approaches.

Pake allows two parties who share a memorable password to securely establish a strong secret key. It has been deployed in many applications around us, such as iCloud service, Wi-Fi access, etc., to provide security assurance for us. In this article, we present a secure and efficient asymmetric PAKE (aPAKE) protocol for protecting the access to the resource-constraint Internet of Things (IoT). Besides the general passive and active attacks, the new aPAKE protocol provides resilience to the offline dictionary attack, and the server compromise attack such that an adversary cannot impersonate the client to the server even if it has compromised the corresponding server and obtained the stored password file. The new aPAKE protocol is detailed in the elliptic curve setting in this article, while it is also compatible with the multiplicative group over a finite field. The security proof for the new aPAKE protocol is carried out in the widely accepted acrshort BPR security model under the basic acrshort CDH security assumption, which implies that our new aPAKE protocol has certain security advantages over some others whose security proofs need to be based on some stronger security assumptions. In addition, the new aPAKE protocol has computational efficiency and ease-of-implementation advantages over some existing aPAKE protocols whose constructions require the use of the hash-to-curve (H2C) function, and the performance evaluation results have definitely shown this fact.

SAE, short for Simultaneous Authentication of Equals, is a password-authenticated key exchange (PAKE) protocol, by which the two involved parties can achieve mutual authentication and derive high-entropy keys via a memorable password. Currently, the SAE protocol has been standardized and integrated into the latest WPA3 (Wi-Fi Protected Access 3) specifications for protecting Wi-Fi network access. Whereas, SAE is a symmetric PAKE protocol unable to resist the server compromise attacks, and it involves explicit key confirmation flows which may be redundant for usage in existing protocols such as the TLS 1.3, etc. So, we naturally wonder that if we can construct a provably secure one-round asymmetric PAKE from the distinguished SAE. This paper affirms this by presenting an efficient asymmetric variant of SAE, called SAE+, and backing it up with a formal security proof under the widely accepted BPR security model. The new SAE+ is designed to enable a single round-trip execution, with the client initiating the communication, making it an ideal fit for integration into IETF protocols such as TLS 1.3. This feature aligns with the requirements set forth in the “Usage of PAKE with TLS 1.3" document. The SAE+ is secure against the off-line dictionary and server compromise attacks, and supports the desired forward secrecy, i.e., compromising the long-term secret password does not compromise the secrecy of the previously established session keys. In addition, the performance evaluation results presented in this paper demonstrate that the new SAE+ has comparable computational efficiency with some existing outstanding PAKE protocols while outperforms many of them in terms of communication flows.

Greetings and a warm welcome to the 2023 32nd IEEE Asian Test Symposium (ATS 2023)!

Ensuring privilege transition integrity during execution context switch is crucial for protecting the processor from unauthorized access and malicious actions. However, existing methods fall short in covering potential attack paths and vectors in a complete manner. In this work, we propose a method for formal verification of privilege correctness targeting privilege escalation attacks, where the program processes on non-privileged mode may access the sensitive information stored in Special purpose registers (SPRs). We specify assertion property and utilize the Klee symbolic execution engine to formally check the consistency in privilege when accessing contents in critical registers. The formal solver performs state space exploration through heuristic search to identify the possible integrity violation test cases that can trigger an illegal privilege escalation, which further allows creating a minimal simulation system consisting of the CPU and Quick Memory (QMEM) modules to replay the privilege violation process. Experimental results have demonstrated that our method can systematically verify the privilege validity to protect the system from privilege escalation attacks on a RISC-V processor.

Software attacks that exploit the hardware security vulnerabilities of processors have become new breakthrough points for hackers, which pose severe threats to hardware security and trust. This paper proposes a novel system security verification method based on instruction set architecture (ISA) level information flow tracking (IFT), which is capable of modeling and checking security properties in both software and hardware designs. We use RISC-V system as a demonstration, which is a lately developed open-source ISA widely used in Internet of Things and is facing severe security threats due to the universal interconnection of devices. By developing RISC-V software and hardware IFT models, security properties including confidentiality and integrity can be verified and vulnerabilities can be detected. Experimental results show that the proposed verification method can detect software security threats and hardware security vulnerabilities in the RISC-V processor design.

Trojan horses represent a major threat to hardware security and trust. In this work, we propose a novel hardware Trojan detection method based on explainable graph neural networks (GNNs) targeting FPGA netlists. We leverage the rich explicit structural features and behavioral characteristics at LUT, which offers an ideal abstraction level and granularity for Trojan detection. A GNN model with optimized class-balanced focal loss is trained for automated Trojan feature extraction and classification. Based on the Granger causality theory, we develop an interpretable approach to explain the decision mechanism of our GNN model. Experimental evaluations using 927 Trust-Hub hardware Trojan benchmarks and 262 Trojan free open source IP cores show that the proposed method provides promising detection results with accuracy, precision and F1-measure of 98.78%, 99.69% and 99.23% for Xilinx FPGA netlists while 97.93%, 97.87% and 98.51% for Intel FPGA netlists respectively. The experiment results have demonstrated that the proposed explainable approach can successfully identify the essential components that contribute to accurate Trojan classification and provide interpretable explanation for the GNN model.

As hardware designs become more complex and incorporate a wider variety of third-party IP cores, the risk of hardware Trojan insertion increases. While several techniques have been introduced to detect hardware Trojans, machine learning-based detection methods rely on a proper feature selection algorithm and learning model. This paper presents a hardware Trojans detection method for gate-level netlists using the stacking ensemble learning method. The study analyzes the essential attributes and common structures of hardware Trojans and proposes inv_x as inverter features to detect ring oscillator circuits. By incorporating the proposed features with the existing attributes, the feature set comprises 56 features. Thus, a hybrid feature selection method that employs Random Forest (RF) and Recursive Feature Elimination with Cross-Validation (RFECV) is proposed to identify the optimal feature set To improve Trojan detection’s accuracy, a stacking ensemble learning model is developed by integrating multiple machine learning classifiers. Finally, we utilize multidimensional data visualization and distance measurement to analyze the detection results. Experimental evaluations using Trust-Hub benchmarks show promising Trojan detection results with the average TPR of 94.15%, the average Fscore of 95.36%, and the average Precision of 96.93%. These results demonstrate a significant improvement over existing hardware Trojan detection methods.

State-of-the-art EDA tools largely employ functional circuit models that are inadequate for verifying and emulating design properties related to fault effect and tolerance. In this paper, we derive fully synthesizable fault effect propagation models for formally reasoning about fault-related design behaviors under different types of faults. We associate each signal bit with a binary fault label to reflect its fault attribute. We further derive fine-granularity precise propagation policies and specify these policies as formal models for fault effect analysis using functional EDA tools. Experimental results using IWLS benchmarks have demonstrated that our formal models can be used to measure fault propagation effects and accelerate fault verification through hardware emulation. Our work makes a step towards property driven EDA flows that allow fault tolerance and dependability to be verified alongside functional correctness.

Hardware security and trust have become a pressing issue during the last two decades due to the globalization of the semiconductor supply chain and ubiquitous network connection of computing devices. Computing hardware is now an attractive attack surface for launching powerful cross-layer security attacks, allowing attackers to infer secret information, hijack control flow, compromise system root-of-trust, steal intellectual property (IP), and fool machine learners. On the other hand, security practitioners have been making tremendous efforts in developing protection techniques and design tools to detect hardware vulnerabilities and fortify hardware design against various known hardware attacks. This article presents an overview of hardware security and trust from the perspectives of threats, countermeasures, and design tools. By introducing the most recent advances in hardware security research and developments, we aim to motivate hardware designers and electronic design automation tool developers to consider the new challenges and opportunities of incorporating an additional dimension of security into robust hardware design, testing, and verification.

Taint-propagation and X-propagation analyses are important tools for enforcing circuit design properties such as security and reliability. Fundamental to these tools are effective models for accurately measuring the propagation of information and calculating metadata. In this work, we formalize a unified model for reasoning about taint- and X-propagation behaviors and verifying design properties related to these behaviors. Our model are developed from the perspective of information flow and can be described using standard hardware description language (HDL), which allows formal verification of both taint-propagation (i.e., security) and X-propagation (i.e., reliability) related properties using standard electronic design automation (EDA) verification tools. Experimental results show that our formal model can be used to prove both security and reliability properties in order to uncover unintended design flaw, timing channel and intentional malicious undocumented functionality in circuit designs.

With the rapid advancements of the artificial intelligence, machine learning, especially neural networks, have shown huge superiority over humans in image recognition, autonomous vehicles and medical diagnosis. However, its opacity and inexplicability provide many chances for malicious attackers. Recent researches have shown that neural networks are vulnerable to adversarial example (AE) attacks. In the testing stage, it fools the model by adding subtle perturbations to the original sample to misclassify the input, which poses a serious threat to safety-critical areas such as autonomous driving. In order to mitigate this threat, this paper proposes a hardware-assisted randomization method against AEs, where an approximate computing technique in hardware, voltage over-scaling (VOS), is used to randomize the training set of the model, then the processed data are used to generate multiple neural network models, finally multiple redundant models are used for the integrated classification and detection of the AEs. Various AE attacks on the proposed defense are evaluated to prove its effectiveness.

Albeit very appealing, FPGA multitenancy in the cloud computing environment is currently on hold due to a number of recently discovered vulnerabilities to side-channel attacks and covert communication. In this work, we successfully demonstrate a new attack scenario on shared FPGAs: we show that an FPGA tenant can activate a dormant hardware Trojan without any physical or logical connection to the private Trojan-infected FPGA circuit. Our victim contains a so-called satisfiability don't-care Trojan, activated by a pair of don't-care signals, which never reach the combined trigger condition under normal operation. However, once a malicious FPGA user starts to induce considerable fluctuations in the on-chip signal delays—and, consequently, the timing faults-these harmless don't-care signals take unexpected values which trigger the Trojan. Our attack model eliminates the assumption on physical access to or manipulation of the victim design. Contrary to existing fault and side-channel attacks that target unprotected cryptographic circuits, our new attack is shown effective even against provably well-protected cryptographic circuits. Besides demonstrating the attack by successfully leaking the entire cryptographic key from one unprotected and one masked AES S-box implementation, we present an efficient and lightweight countermeasure.

Static Random Access Memory (SRAM) is a core technology for building computing hardware, including cache memory, register files and field programmable gate array devices. Hence, SRAM reliability is essential to guarantee dependable computing. While significant research has been conducted to develop automated test algorithms for detecting manufacture-induced SRAM faults, they cannot ensure detection of faults deliberately implemented in the SRAM array by untrusted parties in the integrated circuit development flow. Indeed, such hardware Trojan attacks represent an emerging security threat. While a growing body of research addresses Trojan designs in logic circuits, little research has explored hardware Trojan attacks in embedded memory arrays [20]. In this article, we propose a new class of hardware Trojans targeting embedded SRAM arrays. The Trojans are designed to evade industry standard post-manufacturing tests while enabling attacks targeting various system hardware components during deployment. Transistor-level simulation results demonstrate minimal impact on SRAM power, performance, and stability while Trojans are not activated. We also prove the feasibility of Trojan insertion in foundries by showing the proposed layouts that preserve the SRAM cell footprint and incur zero silicon area overhead. Finally, we elaborate on several system-level attacks that can leverage these Trojans to compromise security and privacy.

High-level synthesis (HLS) allows hardware designers to think algorithmically and not worry about low-level, cycle-by-cycle details. This provides the ability to quickly explore the architectural design space and tradeoffs between resource utilization and performance. Unfortunately, security evaluation is not a standard part of the HLS design flow. In this article, we aim to understand the effects of memory-based HLS optimizations on power side-channel leakage. We use Xilinx Vivado HLS to develop different cryptographic cores, implement them on a Spartan-6 FPGA, and collect power traces. We evaluate the designs with respect to resource utilization, performance, and information leakage through power consumption. We have two important observations and contributions. First, the choice of resource optimization directive results in different levels of side-channel vulnerabilities. Second, the partitioning optimization directive can greatly compromise the hardware cryptographic system through power side-channel leakage due to the deployment of memory control logic. We describe an evaluation procedure for power side-channel leakage and use it to make best-effort recommendations about how to design more secure architectures in the cryptographic domain.

High-level synthesis (HLS) allows hardware designers to think algorithmically and not have to worry about low-level, cycle-by-cycle details. This provides the ability to quickly explore the architectural design space and tradeoff between resource utilization and performance. Unfortunately, evaluating the security is not a standard part of the HLS design flow. In this work, we aim to understand the effects of HLS optimizations with respect to power side-channel leakage. We use Vivado HLS to develop different cryptographic cores, implement them on a Xilinx Spartan 6 FPGA, and collect power traces. We evaluate the designs with respect to resource utilization, performance, and side-channel leakage through power consumption. Furthermore, we analyze the first-order leakage of the HLS-based designs alongside well-known register transfer level (RTL) cryptographic cores. We describe an evaluation procedure for hardware designers and use it to make insightful recommendations on how to design the best architecture in cryptographic domain.

Hardware information flow analysis detects security vulnerabilities resulting from unintended design flaws, timing channels, and hardware Trojans. These information flow models are typically generated in a general way, which includes a significant amount of redundancy that is irrelevant to the specified security properties. In this work, we propose a property specific approach for information flow security. We create information flow models tailored to the properties to be verified by performing a property specific search to identify security critical paths. This helps find suspicious signals that require closer inspection and quickly eliminates portions of the design that are free of security violations. Our property specific trimming technique reduces the complexity of the security model; this accelerates security verification and restricts potential security violations to a smaller region which helps quickly pinpoint hardware security vulnerabilities.

Cryptographic cores are known to leak information about their private key due to runtime variations, and there are many well-known attacks that can exploit this timing channel. In this paper, we study how information theoretic measures can quantify the amount of key leakage that can be exacted from runtime measurements. We develop and analyze 22 Rivest-Shamir-Adleman (RSA) hardware designs-each with unique performance optimizations, timing channel mitigation techniques, or discretization/randomization countermeasures. We demonstrate the effectiveness of information theoretic measures for quantifying timing leakage through correlation analysis of information theoretic measurements and attack results. Experimental results show that mutual information is a promising technique for quantifying timing leakage for RSA, advanced encryption standard, and elliptic curve cryptography ciphers, i.e., the mutual information correlates to being able to successfully guess the value of the private key. This is an important step toward a hardware security metric which allows designers to reason about security alongside traditional hardware design metrics like area, performance, and power.

Hardware has become an increasingly attractive target for attackers, yet we still largely lack tools that enable us to analyze large designs for security flaws. Information flow tracking (IFT) models provide an approach to verifying a hardware design's adherence to security properties related to isolation and reachability.

Information Flow Tracking (IFT) provides a formal methodology for modeling and reasoning about security properties related to integrity, confidentiality, and logical side channel. Recently, IFT has been employed for secure hardware design and verification. However, existing hardware IFT techniques either require designers to rewrite their hardware specifications in a new language or do not scale to large designs due to a low level of abstraction. In this work, we propose Register Transfer Level IFT (RTLIFT), which enables verification of security properties in an early design phase, at a higher level of abstraction, and directly on RTL code. The proposed method enables a precise understanding of all logical flows through RTL design and allows various tradeoffs in IFT precision. We show that RTLIFT achieves over 5x speedup in verification performance as compared to gate level IFT while minimizing the required effort for the designer to verify security properties on RTL designs.

Emergence of side channel security attacks has challenged the classic assumptions regarding what data is publicly available. As demonstrated repeatedly, statistical analysis of information collected by measuring completion time of hardware designs can reveal confidential information. Even though timing-based side channel leakage can be easily exploited to breach data privacy, conventional hardware verification tools are not yet suited to assess these vulnerabilities. To acquaint the hardware design process with formal security evaluations, we introduce a model for tracking timing-based information flows through HDL codes. Based on this model, we have developed Clepsydra, a tool for automatically generating circuitry for tracking timing flows and generic logical flows within hardware designs in two distinct channels. The circuit generated by Clepsydra can be analyzed by EDA tools to detect timing leakage or formally prove constant execution time. We present proofs regarding soundness and precision of the proposed model along with results of employing Clepsydra to verify security properties on a variety of hardware units including crypto cores, bus architectures, caches and arithmetic modules.

Hardware Trojans are a significant security threat due to the globalization of hardware design and supply chain. We demonstrate a new type of hardware Trojan hidden behind internal don't care conditions. The proposed Trojans can pass through formal equivalence checking; they may reside after logic synthesis optimizations; and they are resilient to switching probability and side channel analysis. The new Trojans can create a surface for fault attack to retrieve secret information or downgrade performance by increasing power consumption. Experimental results show that these Trojans may stay after logic synthesis and that secret information can be retrieved using fault attack. We present detectability analysis and suggest synthesis optimizations as well as countermeasures that can help mitigate this new Trojan.

Secure hardware design is a challenging task that goes far beyond ensuring functional correctness. Important design properties such as non-interference cannot be verified on functional circuit models due to the lack of essential information (e.g., sensitivity level) for reasoning about security. Hardware information flow tracking (IFT) techniques associate data objects in the hardware design with sensitivity labels for modeling security-related behaviors. They allow the designer to test and verify security properties related to confidentiality, integrity, and logical side channels. However, precisely accounting for each bit of information flow at the hardware level can be expensive. In this work, we focus on the precision of the IFT logic. The key idea is to selectively introduce only one sided errors (false positives); these provide a conservative and safe information flow response while reducing the complexity of the security logic. We investigate the effect of logic synthesis on the quality and complexity of hardware IFT and reveal how different logic synthesis optimizations affect the amount of false positives and design overheads of IFT logic. We propose novel techniques to further simplify the IFT logic while adding no, or only a minimum number of, false positives. Additionally, we provide a solution to quantitatively introduce false positives in order to accelerate information flow security verification. Experimental results using IWLS benchmarks show that our method can reduce complexity of GLIFT by 14.47% while adding 0.20% of false positives on average. By quantitatively introducing false positives, we can achieve up to a 55.72% speedup in verification time.

Cryptographic function implementations are known to leak information about private keys through timing information. By using statistical analysis of the variations in runtime required to encrypt different messages, an attacker can relatively easily determine the key with high probability. There are many mitigation techniques to combat these side channels; however, there are limited metrics available to quantify the effectiveness of these mitigation attacks. In this work, we employ information theoretic ideas to quantify the amount of leakage that can be extracted from runtime measurements and reveal the influence of individual key bits on the timing observations across a variety of hardware implementations. By studying different RSA hardware architectures (each with different performance optimizations and mitigation techniques), we determine the effectiveness of these information theoretic techniques against the success of attacks. Our experimental results show that mutual information is a promising metric to quantify timing-based information leakage and it also correlates to the attack-ability of a cryptographic implementation.

With the wide deployment of embedded systems and constant increase in their inter‐connections, embedded systems tend to be confronted with attacks through security holes that are hard to predict using typical security measures such as access control or data encryption. To eliminate these security holes, embedded security should be accounted for during the design phase from all abstraction levels with effective measures taken to prevent unintended interference between different system components caused by harmful flows of information. This study proposes a bottom‐up approach to designing verifiably information flow secure embedded systems. The proposed method enables tight information flow controls by monitoring all flows of information from the level of Boolean gates. It lays a solid foundation to information flow security in the underlying hardware and exposes the ability to prove security properties to all abstraction levels in the entire system stack. With substantial amounts of modifications made to the instruction set architecture, operating system, programming language and input/output architecture, the target system can be designed to be verifiably information flow secure.

High-assurance systems found in safety-critical infrastructures are facing steadily increasing cyber threats. These critical systems require rigorous guarantees in information flow security to prevent confidential information from leaking to an unclassified domain and the root of trust from being violated by an untrusted party. To enforce bit-tight information flow control, gate-level information flow tracking (GLIFT) has recently been proposed to precisely measure and manage all digital information flows in the underlying hardware, including implicit flows through hardware-specific timing channels. However, existing work in this realm either restricts to two-level security labels or essentially targets two-input primitive gates and several simple multilevel security lattices. This article provides a general way to expand the GLIFT method for multilevel security. Specifically, it formalizes tracking logic for an arbitrary Boolean gate under finite security lattices, presents a precise tracking logic generation method for eliminating false positives in GLIFT logic created in a constructive manner, and illustrates application scenarios of GLIFT for enforcing multilevel information flow security. Experimental results show various trade-offs in precision and performance of GLIFT logic created using different methods. It also reveals the area and performance overheads that should be expected when expanding GLIFT for multilevel security.

High assurance systems require strict guarantees on information flow security and fault tolerance or else face catastrophic consequences. Recently, Gate Level Information Flow Tracking (GLIFT) has been proposed to monitor information flows at the level of Boolean logic. At this level, all flows are explicit which makes it possible to detect security violations, even those that occur due to difficult to detect timing channels. In this paper, we show that the encoding technique used in previous GLIFT generation methods includes redundant encoding states, which leads to large overheads in area, delay and verification time. We present a new encoding technique with fewer encoding states by leveraging an inherent property of GLIFT. By denoting don't-care input conditions to logic synthesis tools, smaller GLIFT logic for dynamic information flow tracking is obtained and shorter simulation time for static information flow security verification is achieved. Experimental results using the IWLS benchmarks show average reductions of 39.8%, 31.1% and 57.5% in area, delay and simulation time respectively. Furthermore, the new encoding technique enables the GLIFT tracking logic to function both as information flow tracking and redundant logic. As a result, information flow security and fault tolerance can be simultaneously enforced with the same logic.

Hardware-based side channels are known to expose hard-to-detect security holes enabling attackers to get a foothold into the system to perform malicious activities. Despite this fact, security is rarely accounted for in hardware design flows. As a result, security holes are often only identified after significant damage has been inflicted. Recently, gate level information flow tracking (GLIFT) has been proposed to verify information flow security at the level of Boolean gates. GLIFT is able to detect all logical flows including hardware specific timing channels, which is useful for ensuring properties related to confidentiality and integrity and can even provide real-time guarantees on system behavior. GLIFT can be integrated into the standard hardware design, testing and verification process to eliminate unintended information flows in the target design. However, generating GLIFT logic is a difficult problem due to its inherent complexity and the potential losses in precision. This paper provides a formal basis for deriving GLIFT logic which includes a proof on the NP-completeness of generating precise GLIFT logic and a formal analysis of the complexity and precision of various GLIFT logic generation algorithms. Experimental results using IWLS benchmarks provide a practical understanding of the computational complexity.

Flight control, banking, medical, and other high assurance systems have a strict requirement on correct operation. Fundamental to this is the enforcement of non-interference where particular subsystems should not affect one another. In an effort to help guarantee this policy, recent work has emerged with tracking information flows at the hardware level. This article uses a specific method known as gate-level information flow tracking (GLIFT) to provide a methodology for testing information flows in two common bus protocols, I2C and USB. We show that the protocols do elicit unintended information flows and provide a solution based on time division multiple access (TDMA) that provably isolates devices on the bus from these flows. This paper also discusses the overheads in area and simulation time incurred by this TDMA based solution.

Information flow tracking is an effective tool in computer security for detecting unintended information flows. However, software based information flow tracking implementations have drawbacks in preciseness and performance. As a result, researchers have begun to explore tracking information flow in hardware, and more specifically, understanding the interference of individual bits of information through logical functions. Such gate level information flow tracking (GLIFT) can track information flow in a system at the granularity of individual bits. However, the theoretical basis for GLIFT, which is essential to its adoption in real applications, has never been thoroughly studied. This paper provides fundamental analysis of GLIFT by introducing definitions, properties, and the imprecision problem with a commonly used shadow logic generation method. This paper also presents a solution to this imprecision problem and provides results that show this impreciseness can be tolerated for the benefit of lower area and delay.

Understanding the flow of information is an important aspect in computer security. There has been a recent move towards tracking information in hardware and understanding the flow of individual bits through Boolean functions. Such gate level information flow tracking (GLIFT) provides a precise understanding of all flows of information. This paper presents a theoretical analysis of GLIFT. It formalizes the problem, provides fundamental definitions and properties, introduces precise symbolic representations of the GLIFT logic for basic Boolean functions, and gives analytic and quantitative analysis of the GLIFT logic.