More Like this

1. The K2 Architecture for Trustworthy Hardware Security Modules

   https://doi.org/10.1145/3625275.3625402  

   Athalye, Anish; Kaashoek, Frans; Zeldovich, Nickolai; Tassarotti, Joseph (October 2023, ACM)

   K2 is a new architecture and verification approach for hardware security modules (HSMs). The K2 architecture's rigid separation between I/O, storage, and computation over secret state enables modular proofs and allows for software development and verification independent of hardware development and verification while still providing correctness and security guarantees about the composed system. For a key step of verification, K2 introduces a new tool called Chroniton that automatically proves timing properties of software running on a particular hardware implementation, ensuring the lack of timing side channels at a cycle-accurate level. 

   more » « less
2. Bridging Hardware and Software Through Causality Inference

   Liu, Zhaoxiang; Chen, Kejun; Sullivan, Dean; Arias, Orlando; Guo, Xiaolong (April 2024, New England Hardware Security Days)

   We propose Microscope, a new framework that addresses growing security issues in System-on-Chip (SoC) designs due to their complexity and involvement of third-party vendors. Traditional methods are inadequate for identifying software-exploited hardware vulnerabilities, and existing solutions for hardware-software co-verification often fall short. The framework has been proven effective through extensive testing on SoC benchmarks, and it has outperformed existing methods and commercial tools in comparative analyses. Index Terms—Causality Inference, Hardware Security, 

   more » « less
3. Hardware and Software Co-Verification from Security Perspective

   https://doi.org/10.1109/MTV48867.2019.00018  

   Chen, Kejun; Deng, Qingxu; Hou, Yumin; Jin, Yier; Guo, Xiaolong (December 2019, 2019 20th International Workshop on Microprocessor/SoC Test, Security and Verification (MTV))

   Attacks which combine software vulnerabilities and hardware vulnerabilities are emerging security problems. Although the runtime verification or remote attestation can determine the correctness of a system, existing methods suffer from inflexible security policy setup and high performance overheads. Meanwhile, they rarely focus on addressing the threat in the RISC-V architecture, which provides an open Instruction Set Architecture (ISA) of the processsor. In this paper, we propose a comprehensive software and hardware co-verification method to protect the entire RISC-V system in the runtime. The proposed method adopts the Dynamic Information Flow Tracking (DIFT) framework to implement a new Verifier and Prover security architecture for supporting runtime software and hardware coverification. We realize a FPGA prototype on the Rocket-Chip, an RISC-V open-source processor core. The framework is implemented as a co-processor which do not change the architecture of main processor core and the new security architecture can be integrated with other RISC-V processors. 

   more » « less
4. Microscope: Causality Inference Crossing the Hardware and Software Boundary from Hardware Perspective

   Liu, Zhaoxiang; Chen, Kejun; Sullivan, Dean; Arias, Orlando; Dutta, Raj Gautam; Jin, Yier; Guo, Xiaolong (April 2024, Proceedings of the ASPDAC Asia and South Pacific Design Automation Conference)

   The increasing complexity of System-on-Chip (SoC) designs and the rise of third-party vendors in the semiconductor industry have led to unprecedented security concerns. Traditional formal methods struggle to address software-exploited hardware bugs, and existing solutions for hardware-software co-verification often fall short. This paper presents Microscope, a novel framework for inferring software instruction patterns that can trigger hardware vulnerabilities in SoC designs. Microscope enhances the Structural Causal Model (SCM) with hardware features, creating a scalable Hardware Structural Causal Model (HW-SCM). A domain-specific language (DSL) in SMT-LIB represents the HW-SCM and predefined security properties, with incremental SMT solving deducing possible instructions. Microscope identifies causality to determine whether a hardware threat could result from any software events, providing a valuable resource for patching hardware bugs and generating test input. Extensive experimentation demonstrates Microscope's capability to infer the causality of a wide range of vulnerabilities and bugs located in SoC-level benchmarks. 

   more » « less
5. HADA: Hardware Assertion through Data Augmentation

   Fu, Weimin; Wang, Yiting; Lu, Zelin; Guo, Xiaolong; Qu, Gang (June 2025, IEEE Design Automation Conference (DAC) 2025)

   Hardware security verification in hardware design has been identified as a significant bottleneck due to complexity and time-to-market constraints. Assertion-Based Verification is a recognized solution to this challenge; however, assertion generation relies on expertise and labor. While LLMs show promise as automated tools, existing approaches often rely on complex prompt engineering, requiring expert validation. The challenge lies in identifying effective methods for constructing training datasets that enhance LLMs' hardware performance. We introduce HADA (Hardware Assertion through Data Augmentation), a novel framework to train hardware debug specific expert LLM by leveraging its ability to integrate knowledge from formal verification tools, hardware security knowledge database, and version control system. Our results demonstrate that integrating multi-source data significantly enhances the effectiveness of hardware security verification, with each addressing the limitations of the others. 

   more » « less