Logic locking and hardware Trojans are two fields in hardware security that have been mostly developed independently from each other. In this paper, we identify the relationship between these two fields. We find that a common structure that exists in many logic locking techniques has desirable properties of hardware Trojans (HWT). We then construct a novel type of HWT, called Trojans based on Logic Locking (TroLL), in a way that can evade state-of-the-art ATPG-based HWT detection techniques. In an effort to detect TroLL, we propose customization of existing state-of-the-art ATPG-based HWT detection approaches as well as adapting the SAT-based attacks on logic locking to HWT detection. In our experiments, we use random sampling as reference. It is shown that the customized ATPG-based approaches are the best performing but only offer limited improvement over random sampling. Moreover, their efficacy also diminishes as TroLL’s triggers become longer (i. e. have more bits specified). We thereby highlight the need to find a scalable HWT detection approach for TroLL.

While there is explosive growth in the creation of biological data, researchers rely on ad hoc verification methods such as testing with small simulated datasets. Due to their importance in biology and biomedicine, there is a critical need to verify these algorithms as well as their implementations to ensure that the results and conclusions are trustworthy. In this paper, we explore an effective combination of model checking and theorem proving of bioinformatics software, including BiopLib, BWA, Jellyfish, SDSL, Dashing, SPAdes, and MUMmer. We provide results for model checking for bioinfomatics software libraries and theorem proving for specific properties. Our model checking framework found several potential flaws in the two tools (BiopLib and BWA). We have also detected several failing cases in Succinct Data Structures Library (SDSL).

Software based cryptographic implementations provide flexibility but they face performance limitations. In contrast, hardware based cryptographic accelerators utilize application-specific customization to provide real-time security solutions. Cryptographic instruction-set extensions (CISE) combine the advantages of both hardware and software based solutions to provide higher performance combined with the flexibility of atomic-level cryptographic operations. While CISE is widely used to develop security solutions, side-channel analysis of CISE-based devices is in its infancy. Specifically, it is important to evaluate whether the power usage and electromagnetic emissions of CISE-based devices have any correlation with its internal operations, which an adversary can exploit to deduce cryptographic secrets. In this paper, we propose a test vector leakage assessment framework to evaluate the pre-silicon prototypes at the early stages of the design life-cycle. Specifically, we first identify functional units with the potential for leaking information through power side-channel signatures and then evaluate them on system prototypes by generating the necessary firmware to maximize the side-channel signature. Our experimental results on two RISC-V based cryptographic extensions, RISCV-CRYPTO and XCRYPTO, demonstrated that seven out of eight prototype AES- and SHA-related functional units are vulnerable to leaking cryptographic secrets through their power side-channel signature even in full system mode with a statistical significance of$\alpha = 0.05$.

Modern computing devices rely on root-of-trust (RoT) to ensure confidentiality and integrity of both application code and data while satisfying a wide variety of user requirements. The RoT provides essential cryptographic and security functions as services (implemented as system calls) to the host system, supporting the execution of both trusted and untrusted applications. It also enables a secure boot process for the host operating system and other functionalities to establish a trusted execution environment for user applications. The complexity of RoT implementation often introduces vulnerabilities, such as privilege escalation and code injection risks, which affect the security of user data during execution. In this paper, we propose a RoT firmware verification framework that acts as a firmware firewall (FirmWall) to enhance the overall security of the system. Specifically, we perform directed symbolic execution focused on system calls to verify RoT firmware binaries against security specifications, facilitating targeted patching to mitigate potential vulnerabilities. Our framework demonstrated significantly better coverage compared to state-of-the-art symbolic execution. It also confirmed the presence of multiple vulnerabilities (CVEs) in recent versions of ARM Trusted Firmware-M implementations.

Power side-channel attacks are widely known for extracting information from data processed within a device while assuming that an attacker has physical access or the ability to modify the device. In this article, we introduce a novel side-channel vulnerability that leaks data-dependent power variations through physical layer supply voltage coupling (PSVC). Unlike traditional power side-channel attacks, the proposed vulnerability allows an adversary to mount an attack and extract information without modifying the device. In addition, unlike existing power-based remote attacks on field-programmable gate arrays (FPGAs), the PSVC vulnerability applies to both on-chip and on-board attacks. We assess the effectiveness of the PSVC vulnerability through three case studies, demonstrating several end-to-end attacks on general-purpose microcontrollers with varying adversary capabilities. These case studies provide evidence for the existence of the PSVC vulnerability, its applicability to on-chip as well as on-board side-channel attacks, and how it can eliminate the need for physical access to the target device, making it applicable to any off-the-shelf hardware. Our experiments also reveal that designing devices to operate at the lowest operational voltage significantly reduces the risk of PSVC side-channel vulnerability.

Security enclaves provide isolated execution environments for trusted applications. However, modern processors utilize diverse performance enhancement methods (e.g., branch prediction and parallel execution) that can introduce security vulnerabilities. Specifically, if a processor leaks any information, an adversary can monitor and recover secrets from trusted applications. This paper makes a connection between context switching and information leakage in security enclaves. We present an evaluation framework that analyzes the potential channels through which context switching can expose sensitive information across the security enclave boundaries as a physical side-channel signature. Specifically, we propose a statistical information leakage assessment technique to evaluate the side-channel leakage of a security enclave during the pre-silicon design stage. Experimental evaluation on multiple RISC-V security enclaves reveals that context switching introduces power side channels that an adversary can exploit to infer the execution sequences as well as register values of trusted applications.

Hardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. Manual development of abstraction or hints requires domain expertise and can be time-consuming and error-prone, leading to incorrect proofs or inaccurate results. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification. Our proposed approach is applicable to actual firmware and hardware implementations without requiring any manual intervention during formal model generation or hint extraction. To reduce the state space complexity, we utilize both static module-level analysis and dynamic execution of verification scenarios to automatically generate system-level hints. These hints guide the underlying solver to perform scalable equivalence checking using proofs. The extracted hints are validated against the implementation before using them in the proofs. Experimental evaluation on RISC-V based systems demonstrates that our proposed framework is scalable due to scenario-based decomposition and automated hint extraction. Moreover, our fully automated framework can identify complex bugs in actual firmware-hardware implementations.

Concolic testing is a scalable solution for automated generation of directed tests for validation of hardware designs. Unfortunately, concolic testing fails to cover complex corner cases such as hard-to-activate branches. In this article, we propose an incremental concolic testing technique to cover hard-to-activate branches in register-transfer level (RTL) models. We show that a complex branch condition can be viewed as a sequence of easy-to-activate events. We map the branch coverage problem to the coverage of a sequence of events. We propose an efficient algorithm to cover the sequence of events using concolic testing. Specifically, the test generated to activate the current event is used as the starting point to activate the next event in the sequence. Experimental results demonstrate that our approach can be used to generate directed tests to cover complex corner cases in RTL models while state-of-the-art methods fail to activate them.

System-on-Chip (SoC) security is vital in designing trustworthy systems. Detecting and fixing a vulnerability in the early stages is easier and cost-effective. Assertion-based verification is widely used for functional validation of Register-Transfer Level (RTL) designs. Assertions can improve the controllability and observability that can lead to faster error detection and localization. Although assertions are widely used for functional validation of RTL models, there is limited effort in applying assertions to detect SoC security vulnerabilities. Specifically, a fundamental challenge in SoC security and trust validation is how to develop high-quality security assertions. In this article, we perform automated vulnerability analysis of RTL models to generate security assertions for six classes of vulnerabilities. Experimental results show that the generated security assertions can detect a wide variety of vulnerabilities. Our automated framework can drastically reduce the overall security validation effort compared to the manual development of security assertions. Automated generation of security assertions will enable assertion-based verification to be one of the most promising pre-silicon security sign-off solutions.

Semiconductor supply chain vulnerability is a major concern in designing trustworthy systems. Malicious implants, popularly known as hardware Trojans (HTs), can get introduced at different stages in the system-on-chip (SoC) design cycle. While there are promising test generation techniques for HT detection, they have two practical limitations: 1) these approaches are designed to activate rare states while ignoring rare transitions and 2) these approaches are not scalable for large designs. In this article, we propose a scalable test generation framework to address the above challenges. Our threat model assumes that an adversary may exploit rare events consisting of rare signals (states) as well as rare branches (transitions). We show that the rare branch coverage problem can be mapped to the rare signal coverage problem. We propose a scalable framework for detecting HTs using automated test pattern generation (ATPG)-based activation of rare events. Specifically, we utilize the complementary abilities of N-detection and maximal clique activation of rare events to generate efficient test patterns. Experimental evaluation shows that our ATPG-based framework is scalable and significantly outperforms the state-of-the-art test generation-based Trojan detection techniques.

Test vector leakage assessment (TVLA*) evaluates the side-channel leakage of sensitive information from the hardware implementation of a design. While TVLA* for symmetric cryptography has been well studied, it is not applicable to asymmetric cryptography algorithms. Asymmetric-key algorithms involve complex computations in multiple stages that can lead to varying trace lengths depending on input parameters and associated constraints. In this article, we design an effective TVLA* technique for asymmetric-key cryptosystems that can compare lengthy trace data with a good statistical resolution and generate valid input (test) patterns to satisfy specific constraints. Specifically, this article makes the following major contributions. The proposed test generation algorithm can produce valid test patterns to maximize the power signature differences. Our proposed partition-based differential power analysis can significantly improve the TVLA* accuracy. Extensive evaluation using elliptic curve cryptography algorithms demonstrates that the proposed TVLA* framework can handle type 1 and type 2 statistical errors and evaluate hardware implementations of asymmetric cryptography algorithms with a statistical confidence of 99.999%.

Finite State Machines (FSMs) are widely used to implement complex computation sequences and communication protocols. An FSM may consist of different states with different privilege levels, such as protected and non-protected. Ideally, switching from a non-protected state to a protected state should involve an authorization transition. However, with Laser-based Fault injection (LFI), an attacker can bypass authorization by flipping bits in the FSM’s state vector. In order to mitigate LFI vulnerability, one can encode the FSM states with the objective of maintaining a large Hamming Distance (HD) between each pair of states. The existing FSM encoding algorithms are either very slow, rely on the user’s mathematical ability to manually generate certain state encodings, or lead to unacceptable area overhead. In this paper, we propose an automated framework for generating FSM encodings to defend against LFI attacks. The proposed technique is a fast linear code-based heuristic to produce area-efficient results. We also propose an application-specific simplification to further reduce the area overhead. Experimental results demonstrate that our proposed method is several orders-of-magnitude faster than the state-of-the-art approaches. Our approach also significantly reduces the state code length (50% on average) compared to state-of-the-art approaches.