RTL Verification for Secure Speculation Using Contract Shadow Logic

Of course. Here is a peer review of the paper from the perspective of "The Guardian."

---

Review Form

Paper Title: RTL Verification for Secure Speculation Using Contract Shadow Logic

Reviewer: The Guardian

---

Summary

The authors present "Contract Shadow Logic," a formal verification technique for checking secure speculation properties in out-of-order processors at the RTL level. The core idea is to eliminate the need for explicit, separate ISA-level models in the verification setup. Instead, they propose using "shadow logic" to extract the architectural trace directly from two running instances of the out-of-order processor under test. This reduces the four-machine verification problem to a two-machine problem, which they claim significantly improves scalability and reduces the manual effort associated with writing formal invariants. The method is evaluated on several processors, including the BOOM core, and compared against a baseline, LEAVE, and UPEC.

While the approach presents a novel engineering insight, its claims of providing sound security proofs are built on a foundation of questionable assumptions. The methodology decouples security verification from functional verification in a way that is fundamentally unsafe and introduces an intrusive verification mechanism that actively interferes with the microarchitectural behavior of the design under test. The claims of scalability are also overstated, as the experiments demonstrate that the technique still succumbs to exponential state space explosion on key parameters.

Strengths

1. Novel Architectural Insight: The central idea of replacing the two single-cycle ISA machines with ISA trace extraction from the OoO cores is a clever way to reframe the verification problem. It leverages the architectural property that a functionally correct processor's commit stream is, by definition, an ISA-compliant trace.

2. Demonstrated Bug-Finding Efficacy: The paper's strongest contribution is its demonstrated ability to find non-trivial security vulnerabilities (e.g., those related to misaligned memory access and branch misprediction) on a complex, open-source design like BOOM (Section 7.1.4, page 10). Achieving this with only ~240 lines of Verilog for the shadow logic is a notable practical result when contrasted with the tens of thousands of lines of invariants required by UPEC for the same processor.

3. Clarity of Presentation: The paper is well-written and does an effective job of explaining the baseline verification problem, the authors' key insight, and the challenges (Inclusion and Synchronization) that their two-phase logic aims to solve.

Weaknesses

1. Fundamental Methodological Flaw: The Verification Gap. The entire methodology is predicated on a critical and explicitly stated assumption: "the out-of-order processor is assumed to be functionally correct" (Section 5.4, page 8). This assumption is unacceptable for a security proof. A subtle functional bug (e.g., an incorrect data-forwarding path, a corner-case in the re-order buffer logic, or a faulty exception handler) can be the direct cause of a security vulnerability that leaks information speculatively. By assuming functional correctness, the authors are not verifying the actual RTL design; they are verifying an idealized abstraction of it. This completely decouples the security proof from the implementation's correctness, rendering the "proof" unsound. The claim of deriving "complete proofs on secure designs" (Abstract, page 1) is therefore invalid.

2. Intrusive Verification Technique. The proposed "Two-Phase Shadow Logic" is not a passive monitor; it is an active controller that interferes with the design under test. The mechanism to "re-align the ISA observation traces" involves pausing the clock of one of the processor instances (Listing 1, lines 1-2 and 23-30, page 7). The authors' defense of this technique in Section 5.3 (page 7), stating it "does not affect the execution results of committed instructions," misses the point entirely. Security verification for speculative execution is concerned with the transient, microarchitectural process, not just the final architectural result. Pausing one core's clock while the other continues fundamentally alters the relative timing of events and the evolution of the microarchitectural state. This could easily mask timing-based side channels or other vulnerabilities that depend on specific interleavings of events in the two machines. This interference invalidates the claim that the verification environment accurately models the behavior of the real hardware.

3. Overstated Scalability Claims. The abstract claims "considerably improve RTL verification scalability." However, the experimental results show this improvement to be incremental at best, and the approach does not solve the underlying state-explosion problem. Figure 2 (page 11) clearly shows that verification time increases exponentially with the ROB size. Furthermore, Table 2 (page 9) shows that the technique times out when attempting to prove the security of BOOM-S, the secure version of the most complex processor evaluated. While UPEC (with significant effort) could complete this proof, the proposed method failed. This suggests that while Contract Shadow Logic may be a more efficient bug-finder, it does not represent a fundamental breakthrough in scalability for proving security on large designs. The claims should be significantly toned down to reflect this reality.

4. Manual Effort is Shifted, Not Eliminated. The paper heavily criticizes the 20,000 lines of manual invariants needed for UPEC. While their ~100-400 lines of shadow logic is an impressive reduction, the complexity of this logic is non-trivial and its correctness is paramount. For a modern superscalar processor with multiple commit ports, complex exception handling, and a strict memory consistency model, designing and—crucially—validating the shadow logic to correctly extract the ISA trace under all conditions is a highly complex, error-prone manual task. An error in the shadow logic would silently invalidate the entire verification effort. The paper dismisses this as a "straightforward for the processor designers to carry out" (Section 5.1, page 6), but in reality, it swaps one form of expert manual labor (formal methods expertise) for another (deep microarchitectural debugging and validation expertise).

Questions to Address In Rebuttal

1. Regarding the verification gap: How can the authors justify that a proof of security is meaningful when it is conditioned on the assumption of perfect functional correctness, given that functional bugs are themselves a primary source of security vulnerabilities? Does this not limit the tool to only finding security bugs that are independent of any functional bugs?

2. Regarding the intrusive pausing mechanism: Please provide a formal argument for why actively pausing the clock of one processor instance—thereby altering the relative timing and interleaving of all microarchitectural events—does not invalidate the verification of timing-dependent side channels or other transient execution vulnerabilities.

3. Regarding scalability: Given the exponential increase in verification time with ROB size (Figure 2) and the timeout on BOOM-S, how can the claim of "considerably" improved scalability be substantiated? Would it not be more accurate to frame the contribution as a more scalable bug-finding technique rather than a scalable proving technique for complex designs?

4. Regarding manual effort: Could the authors provide a more detailed analysis of the complexity of designing and validating the shadow logic itself? Specifically, how would this logic handle features like out-of-order commits, precise exceptions triggered by in-flight instructions, and interactions with a complex memory subsystem, and what guarantees its own correctness?

Of course. Here is a peer review of the paper from the perspective of "The Synthesizer."

---

Review Form: RTL Verification for Secure Speculation Using Contract Shadow Logic

Summary

This paper presents "Contract Shadow Logic," a novel formal verification methodology for checking secure speculation properties in out-of-order processors at the Register-Transfer Level (RTL). The core contribution is an elegant, architecture-driven insight: instead of verifying a complex microarchitecture against a separate, simple ISA-level model (a "4-machine problem"), the authors propose using lightweight "shadow logic" to extract the architectural (ISA) trace directly from the committed state of the processor under test. This reframes the verification task as a self-comparison between two instances of the processor (a "2-machine problem"), dramatically reducing the state space and improving scalability.

The authors demonstrate their approach on four processors, including the complex BOOM design. Their results show a significant advantage over a baseline verification scheme and two state-of-the-art techniques (LEAVE and UPEC), successfully finding attacks and proving security with substantially less manual effort than existing high-assurance methods.

Strengths

1. A Powerful and Elegant Core Idea: The central concept of leveraging the processor's own commit stage as the "golden reference" for its architectural behavior is both insightful and pragmatic. It correctly intuits that a functionally correct processor already contains a correct ISA machine within its logic. By formalizing this intuition into a verification strategy, the authors create a methodology that is more scalable than the baseline and more architecturally grounded than methods that rely purely on formal invariants.

2. Excellent Positioning within the Literature: The paper does a superb job of identifying and positioning its contribution within the existing landscape of RTL security verification. It clearly articulates the trade-offs between UPEC (high manual effort, high assurance for complex designs) and LEAVE (automated, but struggles with out-of-order complexity). Contract Shadow Logic carves out a compelling and valuable middle ground, aiming to achieve strong assurance with a level of manual effort that is both reasonable and, crucially, aligned with the skillset of a hardware designer.

3. Accessibility for the Target Audience (Hardware Architects): A major strength of this approach is that it bridges the gap between the formal methods and computer architecture communities. The "manual effort" required is not writing thousands of lines of esoteric formal invariants, but rather instrumenting an RTL design to extract specific information upon instruction commit. This is a far more familiar and intuitive task for a verification engineer or architect, potentially lowering the barrier to adoption for formal security analysis in practice.

4. Thorough and Convincing Evaluation: The experimental results presented in Section 7 are compelling. The head-to-head comparison in Table 2 (page 9) clearly demonstrates the limitations of the baseline (times out) and LEAVE (produces false counterexamples) on out-of-order designs where the proposed scheme succeeds. Furthermore, successfully finding known (and new) attack vectors on a complex core like BOOM with only ~240 lines of shadow logic is a powerful testament to the method's efficacy and efficiency compared to the 20,000+ lines of invariants required by UPEC.

Weaknesses

My critiques are less about flaws and more about clarifying the boundaries and assumptions of this promising methodology.

1. The Decoupling of Functional and Security Verification: The authors correctly identify the "Verification Gap" in Section 5.4 (page 8), noting that their approach assumes the functional correctness of the out-of-order processor's commit stage. This is a standard and reasonable decoupling in verification. However, this assumption is fundamental to the entire methodology's soundness. The work would be strengthened by a more detailed discussion of this trade-off. For instance, a subtle functional bug that causes the commit stage to produce an architecturally incorrect trace could, in theory, either mask a real security leak or create a false positive. While functional verification is a separate problem, the interface between it and this security verification scheme is critical.

2. Implicit Scalability Boundaries: The work demonstrates a significant leap in scalability, but it is also transparent about its limits. The results in Section 7.3 (page 12) show that verification time grows exponentially with ROB size, and the scheme still times out when attempting to generate a full proof for the secure BOOM-S configuration. This is not a failure of the paper but an honest confrontation with the inherent difficulty of hardware model checking. This work pushes the boundary of what is tractable, but it is clear that verifying processors with very large, production-scale structures remains an open challenge that this method, on its own, does not fully solve.

3. Complexity of Synchronization Logic: The two-phase logic for handling synchronization, detailed in Section 5.3 (page 7), is a clever solution to a non-trivial problem. However, the mechanism of pausing clocks feels like it could become quite complex to implement correctly in a real-world, multi-clock domain SoC. A deeper discussion on how this approach would extend to superscalar processors with multi-cycle commit operations or more complex memory systems would be beneficial.

Questions to Address In Rebuttal

1. Regarding the "Verification Gap" (Section 5.4), can the authors elaborate on the assumed contract with the functional verification team? Specifically, if a functional bug caused the shadow logic to extract an incorrect ISA trace, how would this manifest? Could it potentially lead to a security proof being declared "passed" on a design that is, in fact, vulnerable due to the interaction of the functional and security bugs?

2. The paper hints at an interesting idea in the Future Work section (Section 8) that the contract constraint itself "indirectly strongly constrains the set of reachable states." This suggests that the shadow logic might be doing more than just checking a property; it might be acting as a powerful, implicit invariant that aids the model checker. Could you expand on this hypothesis? Is it possible that this architectural constraining is a key, perhaps under-emphasized, reason for the observed performance improvement?

3. The proposed future work to integrate taint propagation techniques like GLIFT is very interesting. How do you envision Contract Shadow Logic co-existing with or complementing such an approach? Would the shadow logic be used to define the sources and sinks for taint, or would it serve an entirely different purpose in a combined methodology?

Innovator Review Form

Paper: RTL Verification for Secure Speculation Using Contract Shadow Logic

---

Summary

The authors present "Contract Shadow Logic," a formal verification methodology for checking secure speculation properties on RTL processor designs. The central problem is the high cost and poor scalability of existing verification schemes, which typically require a baseline of four state machines: two microarchitectural designs to check for leakage (a hyperproperty) and two instruction-set architecture (ISA) models to ensure the inputs to the microarchitectural models satisfy the software-level contract.

The claimed novel contribution is a technique to eliminate the two explicit ISA models. The core insight, as detailed in Section 4.2 (page 5), is that a functionally correct out-of-order processor's commit stream is, by definition, an accurate representation of the ISA-level execution trace. The authors propose using "shadow logic" to extract this architectural trace directly from the two microarchitectural models. This reduces the problem from a four-machine comparison to a two-machine comparison with auxiliary logic. A further contribution is the "Two-Phase Shadow Logic" (Section 5.3, page 7), a specific mechanism designed to handle the instruction inclusion and synchronization challenges that arise from comparing the asynchronous commit streams of two out-of-order cores.

Strengths

The primary strength of this paper lies in its central, elegant insight. The proposal to reconstruct the architectural-level contract check from the microarchitectural implementation itself is a conceptually novel simplification for this specific verification problem. It reframes the problem from comparing a DUT against a golden model to a constrained self-comparison.

The identification and solution for the resulting challenges are also novel. The "Instruction Inclusion Requirement" and "Synchronization Requirement" (Section 5.2, page 6) are non-obvious consequences of their core idea. The proposed "Two-Phase Shadow Logic," which uses a clock-gating mechanism to re-align the processors' commit streams after a microarchitectural divergence is detected, is a new and specific technique tailored to solve this problem. This two-phase approach appears to be a genuinely new piece of verification machinery for this domain.

Weaknesses

While the synthesis of the ideas is new, the fundamental building blocks are not, and the paper should be more precise in delineating this.

1. "Shadow Logic" is not Inherently Novel: The concept of adding auxiliary, non-functional logic (shadow/ghost logic) to a design to aid verification is a well-established practice. For instance, the authors themselves cite prior work [51] using it for ISA specification checking in Section 2.4 (page 4). The novelty here is not the use of shadow logic per se, but its specific application to reconstruct an architectural trace for use as a dynamic assumption in a security hyperproperty check. The contribution is the methodology, not the component.

2. Conceptual Overlap with Tandem Verification: The authors correctly identify the similarity to "tandem verification" [74] in their Limitations section (Section 8, page 12). However, this comparison is understated and relegated too late in the paper. The idea of co-simulating two different models (or two copies of the same model) and checking for equivalence at key points is the essence of tandem approaches. The primary delta here is the purpose of the check—enforcing a software contract as an assumption for a security property, rather than checking functional equivalence as the main goal. This distinction is critical and should be made much earlier and more clearly, likely in the background or related work, to properly contextualize the novelty of their scheme.

3. The Synchronization Mechanism: The technique of pausing one of two parallel processes to allow the other to catch up is a standard synchronization pattern in computing. While its application within a two-phase formal verification flow for security appears new, the underlying mechanism is not a fundamentally new algorithm. The novelty is in the trigger (microarchitectural trace deviation) and purpose (enabling a subsequent architectural contract check).

Questions to Address In Rebuttal

1. The paper's novelty hinges on using the extracted ISA trace as a dynamic assumption for the security check. How does the shadow logic for extracting the committed instruction trace differ conceptually from the logic used in end-to-end functional verification tools like isa-formal [51]? Please clarify if the novelty lies purely in using the extracted trace as an assume property rather than an assert property, or if the extraction mechanism itself is fundamentally different.

2. Could the authors elaborate further on the distinction between their approach and tandem verification [74]? Specifically, while tandem verification often compares different abstraction levels (e.g., C++ vs. RTL), how does Contract Shadow Logic differ from a hypothetical tandem verification setup comparing two RTL instances against each other for functional equivalence?

3. The Two-Phase logic is presented as a key enabler. Is this concept of "run until divergence, then pause-and-realign to check a secondary property" a known pattern in the formal verification literature, perhaps under a different name or in a different domain? If so, citations would be appropriate to frame the contribution as a novel application of an existing pattern. If not, the claim to novelty for this mechanism would be strengthened.