A Deductive System for Contract Satisfaction Proofs

This paper introduces a sound and complete deductive proof system based on relative bisimulation and coinductive reasoning to enable modular, interactive verification of hardware-software contract satisfaction, as demonstrated by its formalization in the Rocq proof assistant and application to challenging security proofs.

The Gist

The Big Picture: The "Black Box" Problem

Imagine you are a software developer writing a secret recipe (a program) for a very famous chef (the computer hardware). You want to make sure that no matter who eats the food, they can't figure out your secret ingredients just by watching the chef's movements.

However, the chef is a complex machine. Sometimes, the chef might glance at a secret ingredient, drop a crumb, or move a pot slightly differently depending on what's inside. These tiny "crumbs" are called side-channel leaks. In the real world, hackers use these crumbs to steal passwords and secrets.

To stop this, engineers created Hardware-Software Contracts. Think of these contracts as a "simplified rulebook" for the chef.

• The Contract: Says, "If you see the same public steps, you should see the same public crumbs."
• The Reality: The actual chef (the hardware) is messy and complicated.

The Problem: How do we prove that the messy, real chef actually follows the simplified rulebook? If the contract says "no crumbs," but the real chef drops a crumb, the whole security system fails.

The Old Way: Guessing and Checking

Previously, proving this was like trying to prove a magic trick works by watching it a million times (testing) or trying to simulate every single move in a spreadsheet (model checking).

• The Issue: These methods are slow, prone to computer errors, or require writing thousands of pages of dense math that no one can easily check. It's like trying to prove a bridge is safe by dropping a million cars on it, rather than calculating the physics.

The New Way: The "Interactive Detective" (This Paper)

The authors of this paper built a new tool called a Deductive System. Imagine this as a super-smart, interactive detective game played inside a computer program (called a proof assistant).

Instead of guessing the answer, you and the computer work together to build a logical argument, step-by-step, that guarantees the proof is correct.

The Core Idea: "Relative Trace Equality"

To understand their method, imagine two runners on a track:

1. Runner A (The Contract): Runs on a smooth, perfect track.
2. Runner B (The Hardware): Runs on a bumpy, real-world track.

The goal is to prove: "If Runner A and Runner B look the same from a distance (same steps), then they must also look the same up close (no secret drops)."

The paper introduces a technique called Relative Bisimulation.

• The Metaphor: Imagine you are a referee watching four runners at once:
  • Two runners on the Contract track (Runner A1 and A2).
  • Two runners on the Hardware track (Runner B1 and B2).
  • Scenario: You start Runner A1 and A2 with slightly different secret ingredients. You start B1 and B2 with the same secret ingredients.
  • The Rule: If A1 and A2 end up looking identical (same steps), then B1 and B2 must also end up looking identical.

The "Relative Bisimulation" is a way of checking these four runners simultaneously to ensure they stay in sync, even if they run at different speeds.

The Magic Trick: "Coinduction" and "Up-To" Techniques

The hardest part of this proof is that the runners might get out of sync.

• The Problem: The Contract runner might take a "shortcut" (a step that happens instantly), while the Hardware runner has to walk through a muddy field (taking many steps to do the same thing).
• The Old Way: You had to force them to move exactly at the same time (lockstep), which is impossible if one is fast and the other is slow.
• The New Way (Coinduction): The authors use a technique called Coinduction. Think of this as a "time-traveling hypothesis."
  • Instead of checking every single step from start to finish, you say: "I assume that if we get to a future state where the runners are still in sync, then we are good."
  • You build a "safety net" (an invariant) that catches the runners if they drift apart.
  • Up-To Techniques: This is like having a "cheat code" that lets you skip boring parts of the proof. If you know two runners are essentially the same (symmetry) or if one path leads to another (transitivity), you can jump ahead without re-proving the basics.

The Case Studies: Proving the "Always-Mispredict" Trick

The paper tested their system on two real-world security problems:

1. The "Always-Mispredict" Contract:

   • The Scenario: Modern CPUs try to guess which way a door will open (branch prediction) to save time. If they guess wrong, they have to "undo" the work, but sometimes they leave a "crumb" (leak) behind.
   • The Contract: The rulebook says, "Let's pretend the CPU always guesses wrong and tries both doors." This creates a predictable pattern of crumbs.
   • The Proof: The authors used their system to prove that even if the real CPU guesses correctly sometimes, it never leaks more information than the "always-wrong" contract. It's like proving that a cautious driver (the contract) is always safer than a reckless driver (the hardware), even if the reckless driver sometimes gets lucky.

2. The "Sequential" Contract:

   • The Scenario: Real CPUs do things out of order to be fast (like a chef chopping vegetables while the water boils).
   • The Contract: The rulebook says, "Let's pretend the CPU does everything in strict order, one by one."
   • The Proof: They proved that even though the real CPU is chaotic and fast, it doesn't leak secrets that the strict, slow version wouldn't.

Why This Matters

• Trust: Before, we had to trust that the math was right. Now, we have a computer-verified proof that the math is right.
• Modularity: You can build a proof like Lego blocks. If you prove one part works, you can reuse that block for other proofs.
• Safety: This helps prevent future "Meltdown" and "Spectre" style attacks by giving hardware designers a rigorous way to check their work before they build the chips.

Summary Analogy

Imagine you are trying to prove that a toy car (the contract) behaves exactly like a real race car (the hardware) regarding how much fuel it leaks.

• The old way was to drive both cars 1,000 miles and hope they didn't leak.
• This paper builds a magic simulation room where you can pause time, look at the engines of both cars simultaneously, and mathematically prove that if the toy car leaks nothing, the real car cannot leak anything either, even if the real car is driving faster or taking different turns.

This system makes security proofs less like a guessing game and more like a rigorous, unbreakable logical chain.

Technical Summary

1. Problem Statement

The paper addresses the challenge of verifying Hardware-Software Contracts. These contracts are abstract specifications of a CPU's leakage behavior (side-channel information) at the Instruction Set Architecture (ISA) level. They allow software developers to verify program security (e.g., against Spectre/Meltdown attacks) without needing deep knowledge of microarchitectural details.

For this abstraction to be valid, the hardware must satisfy the contract. Formally, a hardware semantics $H$ satisfies a contract $C$ if:
$$\forall P, \sigma, \sigma', \mu. \llbracket P \rrbracket_C(\sigma) = \llbracket P \rrbracket_C(\sigma') \implies \llbracket P \rrbracket_H(\sigma, \mu) = \llbracket P \rrbracket_H(\sigma', \mu)$$
This means if the contract predicts identical leakage traces for two different inputs, the actual hardware must also produce identical leakage traces.

Challenges in Proving Satisfaction:

• Relational Complexity: The property is a 4-ary hyperproperty, relating two contract traces and two hardware traces simultaneously.
• Asynchronicity: Contract and hardware executions often proceed at different speeds (e.g., a contract might simulate a misprediction step-by-step while hardware executes speculatively, or hardware might execute out-of-order while the contract is sequential).
• Limitations of Existing Methods:
  • Model Checking: Often relies on automated invariant search, which can fail to terminate or provide explanations for failures.
  • Pen-and-Paper Proofs: Highly complex (e.g., 25+ dense pages) and difficult to verify rigorously.
  • Existing Interactive Proofs: Typically require defining complex simulation relations (e.g., 3-way simulations) upfront, which is difficult when no compiler exists between the contract and hardware (as they run the same ISA under different semantics).

2. Methodology

The authors propose a deductive proof system implemented in the Rocq (formerly Coq) proof assistant. The methodology is built on three core pillars:

A. Relative Trace Equality and Relative Bisimulation

The authors abstract the problem to Relative Trace Equality: proving that "trace equality in system A implies trace equality in system B."

• They introduce Relative Bisimulation, a 4-ary relation ($s_1, s_2, h_1, h_2$) that characterizes this implication.
• Key Innovation: Unlike standard bisimulation (which requires lockstep steps), relative bisimulation handles asynchronicity by decoupling contract steps from hardware steps.
  • Contract Steps: Treated inductively. The system allows "skipping" contract steps (unrolling the assumption that contract traces are equal) without requiring the hardware to move.
  • Hardware Steps: Treated coinductively. The system requires proving that hardware leakage is equal before advancing the hardware state.
• Formal Definition: Relative bisimulation is defined as a greatest fixpoint ($\nu$) of a function containing an inner least fixpoint ($\mu$). This alternation of fixpoints is crucial for soundness: it prevents the proof from trivially accepting all states (a problem with naive "relaxed" definitions) while still allowing non-lockstep reasoning.

B. Parameterized Coinduction (Paco)

To make proofs modular and incremental, the system utilizes Parameterized Coinduction.

• Instead of guessing a full invariant relation upfront, the proof system constructs the invariant incrementally during the proof.
• The system uses Proof Quintuples ($R \vdash [s_1, h_1, s_2, h_2]$) to represent the state of a proof, where $R$ is a "guarded hypothesis" (the set of state quadruples accumulated so far).
• Core Rules:
  • C-Step / C-Leak: Advance contract states (inductive) or conclude if contract leakage differs.
  • H-Step: Advance hardware states (coinductive) only if leakage matches.
  • Invariant / Cycle: Allow the accumulation of new state pairs into the hypothesis $R$ and close loops when states re-enter $R$.

C. Up-To Techniques

To simplify complex proofs, the system integrates Up-To Techniques (exploiting symmetry and transitivity).

• Symmetry: Swapping states or replacing states with leakage-equivalent ones.
• Transitivity: Composing proofs by reducing contract leakage or augmenting hardware leakage.
• The authors prove that these techniques are sound when applied mid-proof (even with non-empty hypotheses) by encoding them as "compatible functions" within the Paco framework.

3. Key Contributions

1. Relative Bisimulation: A novel, sound, and complete 4-ary proof technique that handles the asynchronicity between contract and hardware semantics without requiring pre-defined simulation relations.
2. Deductive Proof System: A formal system of inference rules (based on parameterized coinduction) that enables modular, incremental, and interactive proofs of contract satisfaction.
3. Formalization: The entire system is formalized in Rocq, with a machine-checked proof of its soundness and completeness relative to trace equality.
4. Up-To Integration: A systematic method for integrating symmetry and transitivity rules into the deductive system, significantly reducing proof complexity.
5. Case Studies: Successful application of the system to two challenging scenarios:
   • Always-Mispredict Contract: Proving a contract that simulates branch misprediction (speculative execution) satisfies a hardware model with a branch predictor.
   • Sequential Contract: Proving a contract that executes instructions sequentially satisfies a hardware model with out-of-order execution.

4. Results

• Verification of CT-SPEC Concepts: The system successfully validated the core abstractions of the CT-SPEC contract (a leading standard for side-channel verification), specifically the "always-mispredict" and "sequential execution" techniques.
• Proof Complexity Reduction: The use of incremental invariant construction and up-to techniques allowed the authors to manage proofs that would otherwise be intractable or require massive manual invariant guessing.
• Mechanization: The proofs are fully mechanized in Rocq, eliminating the risk of human error found in pen-and-paper proofs and providing a high level of trust compared to model checking.

5. Significance

• Foundational Shift: Moves contract satisfaction verification from a purely automated (model checking) or manual (pen-and-paper) paradigm to a deductive, interactive paradigm. This bridges the gap between high-level security reasoning and low-level microarchitectural details.
• Scalability and Modularity: The incremental nature of the proof system allows developers to build proofs piece-by-piece, reusing lemmas and hypotheses, which is essential for scaling to complex modern CPUs.
• Generalizability: While focused on hardware-software contracts, the concept of Relative Bisimulation and the deductive system are applicable to other 4-ary reasoning problems in security, such as Secure Compilation (preserving non-interference across compilation) and Speculative Non-Interference (SNI).
• Future Directions: The paper outlines paths toward handling non-determinism, nested speculation, and the development of a higher-level program logic to abstract away concrete state details.

In summary, this paper provides a rigorous, machine-checked framework for proving that hardware implementations adhere to security contracts, offering a powerful alternative to model checking and manual verification for side-channel security.