Cross-party formal verification for hardware trust

Abstract

Modern computing systems increasingly depend on hardware as the foundation of system trust. Yet establishing that trust has become substantially more difficult in a semiconductor ecosystem defined by extensive third-party IP reuse, complex system-on-chip integration, tight hardware–software coupling, and globally distributed design, manufacturing, and distribution processes. In such an environment, security threats are no longer confined to isolated implementation bugs within a single module. Instead, vulnerabilities may arise from malicious RTL modifications, unintended interactions among integrated IPs, exploitable dependencies between software and hardware, counterfeit devices introduced into the supply chain, and confidentiality risks during pre-purchase IP evaluation and exchange. Although formal verification remains one of the most powerful approaches for establishing design assurance, existing methods often operate at only a single abstraction level, lose important RTL semantics through synthesis or translation, or implicitly assume trusted relationships among the parties involved. These limitations motivate the need for a broader framework capable of reasoning about hardware trust across both technical abstraction boundaries and organizational trust boundaries. This dissertation addresses that need through a unified perspective on cross-party formal verification for hardware trust. The central premise is that hardware trust must be established progressively across expanding boundaries: first among interacting IPs within an integrated system, then across the hardware–software interface, next across the physical supply chain, and finally across mutually untrusted parties engaged in IP exchange. Rather than treating these settings as unrelated problems, this dissertation shows that they are connected by a common challenge: security-relevant behavior propagates across components, clock cycles, abstraction layers, and stakeholders in ways that conventional verification frameworks do not fully capture. To address this challenge, the dissertation combines formal reasoning, static analysis, causal modeling, RTL security instrumentation, and cryptographic protocols into a coherent methodology for analyzing, verifying, and preserving trust in modern hardware ecosystems. The dissertation first focuses on trust within integrated SoC platforms, where malicious behavior may emerge not from the standalone operation of a single IP core, but from its interaction with other components through shared buses and interconnects. To address this challenge, it develops If-Tracker, an RTL-level static information-flow verification framework that operates directly on hardware descriptions by parsing them into abstract syntax trees and constructing cycle-accurate data-flow graphs. Unlike approaches that merely determine whether a path exists, If-Tracker also extracts the conditions under which information can propagate along that path, enabling the detection of subtle threats such as bus eavesdropping, covert leakage paths, and malicious interconnect manipulation, including TrustZone-related tampering. Because the analysis preserves RTL structure and maps suspicious flows back to source code locations, it improves both the precision and interpretability of SoC-scale security verification. In doing so, this part of the dissertation demonstrates that preserving high-level RTL semantics is essential for scalable and explainable formal analysis of integrated hardware systems. Building on this foundation, the dissertation then extends the notion of trust across the hardware–software boundary, where many hardware vulnerabilities become relevant only when they can be triggered by particular software instructions or firmware behaviors. Existing approaches often struggle in this setting because they either translate hardware into software representations that lose structural fidelity or rely on verification tools that are not designed to expose causal relationships between software actions and hardware failures. To overcome these limitations, the dissertation proposes Microscope, a framework based on a Hardware Structural Causal Model (HW-SCM) that captures multi-cycle causal dependencies among software-controlled inputs, internal hardware signals, and security-critical outcomes. Through a dedicated domain-specific language and SMT-based incremental solving, Microscope infers instruction patterns capable of activating hardware bugs and vulnerabilities. This allows verification to move beyond simple property checking toward causal explanation: the framework not only determines whether a vulnerability is reachable, but also identifies how it can be exercised from the software side. As a result, this work bridges formal verification, exploitability analysis, and test generation, offering a practical way to reason about software-exploited hardware weaknesses. The dissertation next broadens the scope of hardware trust from logical behavior to device authenticity in the supply chain. Even when a design has been thoroughly verified, its value as a root of trust is undermined if counterfeit or tampered integrated circuits can be inserted during fabrication, distribution, or deployment. To address this problem, the dissertation presents Wing-RTL, a lightweight RTL-level attestation framework that automatically embeds watermarks into finite state machines and integrates them with an on-chip watermark controller. This enables a secure attestation protocol through which a verifier can confirm the authenticity of a device without exposing the internal watermark itself. By emphasizing automation, minimal hardware overhead, and compatibility with existing SoC infrastructure, Wing-RTL shows that trust must be preserved not only in design logic, but also in the provenance and authenticity of the physical device that implements that logic. In this sense, the dissertation expands formal hardware assurance beyond design-time verification into the broader lifecycle of hardware deployment and supply-chain security. Finally, the dissertation considers a zero-trust setting in which the hardware asset itself is the subject of commercial exchange. In modern semiconductor development, IP vendors and IP users often need to interact before a legal agreement is finalized: the user wants to verify that an IP core satisfies required properties, while the vendor must protect the design from disclosure. At the same time, the user may also wish to keep their intended application, verification property, or purchasing interest confidential. To address these conflicting requirements, the dissertation proposes BlindMarket, an end-to-end framework for verifiable, confidential, and traceable IP core distribution in zero-trust environments. BlindMarket combines customized hardware-to-formula translation, oblivious design selection, secure two-party computation, privacy-preserving SAT solving, hardware-aware optimization through hw-ppSAT, and ledger-based authorization for traceability. This framework enables users to verify design properties before acquisition without learning the full IP implementation, while also preventing the vendor from learning the user’s selection and verification intent. By doing so, the dissertation extends formal verification into a new role: not only as a technique for proving correctness, but also as a mechanism for enabling secure and privacy-preserving interaction among mutually untrusted stakeholders in the hardware ecosystem. Taken together, these contributions advance a single overarching argument: hardware trust is no longer a property that can be established at one level, by one party, or at one stage of the design flow. It must instead be verified across the full chain of interactions through which hardware is described, integrated, exercised, authenticated, exchanged, and ultimately relied upon. By progressing from inter-IP verification to hardware–software causal inference, to device attestation, and finally to privacy-preserving IP distribution, this dissertation develops a layered methodology for establishing trust in contemporary hardware systems.