More Like this

1. 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
2. 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
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. 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
5. Gables: A Roofline Model for Mobile SoCs

   https://doi.org/10.1109/HPCA.2019.00047  

   Hill, Mark; Janapa Reddi, Vijay (February 2019, 2019 IEEE International Symposium on High Performance Computer Architecture (HPCA))

   Over a billion mobile consumer system-on-chip (SoC) chipsets ship each year. Of these, the mobile consumer market undoubtedly involving smartphones has a significant market share. Most modern smartphones comprise of advanced SoC architectures that are made up of multiple cores, GPS, and many different programmable and fixed-function accelerators connected via a complex hierarchy of interconnects with the goal of running a dozen or more critical software usecases under strict power, thermal and energy constraints. The steadily growing complexity of a modern SoC challenges hardware computer architects on how best to do early stage ideation. Late SoC design typically relies on detailed full-system simulation once the hardware is specified and accelerator software is written or ported. However, early-stage SoC design must often select accelerators before a single line of software is written. To help frame SoC thinking and guide early stage mobile SoC design, in this paper we contribute the Gables model that refines and retargets the Roofline model-designed originally for the performance and bandwidth limits of a multicore chip-to model each accelerator on a SoC, to apportion work concurrently among different accelerators (justified by our usecase analysis), and calculate a SoC performance upper bound. We evaluate the Gables model with an existing SoC and develop several extensions that allow Gables to inform early stage mobile SoC design. 

   more » « less