More Like this

1. Automated Generation of Security Assertions for RTL Models

   https://doi.org/10.1145/3565801  

   Witharana, Hasini; Jayasena, Aruna; Whigham, Andrew; Mishra, Prabhat (January 2023, ACM Journal on Emerging Technologies in Computing Systems)

   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. 

   more » « less
2. Automated Test Generation for Activation of Assertions in RTL Models

   https://doi.org/10.1109/ASP-DAC47756.2020.9045731  

   Lyu, Yangdi; Mishra, Prabhat (January 2020, Asia and South Pacific Design Automation Conference (ASP-DAC))

   A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously. 

   more » « less
3. End-to-End Automated Exploit Generation for Validating the Security of Processor Designs

   https://doi.org/10.1109/MICRO.2018.00071  

   Zhang, Rui; Deutschbein, Calvin; Huang, Peng; Sturton, Cynthia (October 2018, 2018 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO))

   This paper presents Coppelia, an end-to-end tool that, given a processor design and a set of security-critical invariants, automatically generates complete, replayable exploit programs to help designers find, contextualize, and assess the security threat of hardware vulnerabilities. In Coppelia, we develop a hardware-oriented backward symbolic execution engine with a new cycle stitching method and fast validation technique, along with several optimizations for exploit generation. We then add program stubs to complete the exploit. We evaluate Coppelia on three CPUs of different architectures. Coppelia is able to find and generate exploits for 29 of 31 known vulnerabilities in these CPUs, including 11 vulnerabilities that commercial and academic model checking tools can not find. All of the generated exploits are successfully replayable on an FPGA board. Moreover, Coppelia finds 4 new vulnerabilities along with exploits in these CPUs. We also use Coppelia to verify whether a security patch indeed fixed a vulnerability, and to refine a set of assertions. 

   more » « less
4. Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs

   Ryan, Kaki; Sturton, Cynthia (October 2023, TU Wien Academic Press, Wien)

   Nadel, Alexander; Rozier, Kristin Yvonne (Ed.)

   Symbolic execution is a powerful verification tool for hardware designs, in particular for security validation. However, symbolic execution suffers from the path explosion problem in which the number of paths to explore grows exponentially with the number of branches in the design. We introduce a new approach, piecewise composition, which leverages the modular structure of hardware to transfer the work of path exploration to SMT solvers. Piecewise composition works by recognizing that independent parts of a design can each be explored once, and the exploration reused. A hardware design with N independent always blocks and at most b branch points per block will require exploration of O((2^b)N) paths in a single clock cycle with our approach compared to O(2^(bN)) paths using traditional symbolic execution. We present Sylvia, a symbolic execution engine implementing piecewise composition. The engine operates directly over RTL without requiring translation to a netlist or software simulation. We evaluate our tool on multiple open-source SoC and CPU designs, including the OR1200 and PULPissimo RISC-V SoC. The piecewise composition technique reduces the number of paths explored by an order of magnitude and reduces the runtime by 97% compared to our baseline. Using 84 properties from the security literature we find assertion violations in open-source designs that traditional model checking and formal verification tools do not find. 

   more » « less
5. 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