More Like this

1. 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
2. A Temporal Causality Model for SoC-Scale Security Formal Verification at the Hardware-Software Boundary

   Liu, Zhaoxiang; Guo, Xiaolong; Arias, Orlando; Sullivan, Dean; Dutta, Raj (March 2024, GOMACTech 2024)

   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 softwareexploited 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. 

   more » « less
3. Directed Test Generation for Activation of Security Assertions in RTL Models

   https://doi.org/10.1145/3441297  

   Witharana, Hasini; Lyu, Yangdi; Mishra, Prabhat (April 2021, ACM Transactions on Design Automation of Electronic Systems)

   null (Ed.)

   Assertions are widely used for functional validation as well as coverage analysis for both software and hardware designs. Assertions enable runtime error detection as well as faster localization of errors. While there is a vast literature on both software and hardware assertions for monitoring functional scenarios, there is limited effort in utilizing assertions to monitor System-on-Chip (SoC) security vulnerabilities. We have identified common SoC security vulnerabilities and defined several classes of assertions to enable runtime checking of security vulnerabilities. A major challenge in assertion-based validation is how to activate the security 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 on diverse benchmarks demonstrate that the directed tests are able to activate security assertions non-vacuously. 

   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. Isadora: Automated Information Flow Property Generation for Hardware Designs

   https://doi.org/10.1145/3474376.3487286  

   Deutschbein, Calvin; Meza, Andres; Restuccia, Francesco; Kastner, Ryan; Sturton, Cynthia (November 2021, ACM Workshop on Attacks and Solutions in Hardware Security)

   Isadora is a methodology for creating information flow specifications of hardware designs. The methodology combines information flow tracking and specification mining to produce a set of information flow properties that are suitable for use during the security validation process, and which support a better understanding of the security posture of the design. Isadora is fully automated; the user provides only the design under consideration and a testbench and need not supply a threat model nor security specifications. We evaluate Isadora on a RISC-V processor plus two designs related to SoC access control. Isadora generates security properties that align with those suggested by the Common Weakness Enumerations (CWEs), and in the case of the SoC designs, align with the properties written manually by security experts. 

   more » « less