skip to main content

Search for: All records

Creators/Authors contains: "Liu, Zhaoxiang"

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. 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
    Free, publicly-accessible full text available April 1, 2025
  2. Hardware IP verification requires collaboration from several parties, including the 3PIP vendor, IP user, and EDA tool vendor, all of whom could threaten the design's integrity and confidentiality. Various frameworks and tools, including the IEEE 1735 standard, have been developed to address these concerns. However, these solutions fall short of the zero trust model's requirements. To overcome this, we propose a novel zero trust formal verification framework that incorporates secure multiparty computation to ensure the privacy of all the parties involved in the verification process. The efficiency of the framework is demonstrated by checking various open-source IP-level benchmarks. 
    more » « less