Leakage Contracts

Overview

Leakage contracts are a security abstraction introduced at the Instruction Set Architecture (ISA) level to formally specify the side-channel leakage behavior of processors. They capture the information a processor may leak via microarchitectural side channels, serving as a single source of truth for verifying both hardware compliance and software security. By decoupling hardware and software verification through a shared contract, they enable modular analysis: any program verified against a contract can run safely on any processor verified against the same contract.

Formal Definition

A leakage contract is a program written in a Turing-complete language (typically C-like) that specifies:

• The functional behavior of an instruction on the processor (ISA-level state transitions)
• The leakage behavior — what information an adversary can observe during execution

The contract's value storage is partitioned into two parts:

• σ: the ISA state (e.g., program counter, architectural registers)
• λ: the accumulated leakage trace visible to an adversary

Leaks are emitted through a special variadic function leak(v1, ..., vn), which appends the concatenation of its arguments to λ. Since leakage cannot disappear, λ only accumulates over execution. The small-step operational semantics of a contract execution are denoted:

⟨σⱼ, λⱼ⟩ →⟨ₙ⟩ ⟨σₙ, λₙ⟩

representing n consecutive instruction executions from initial state σ₀, producing final state σₙ and accumulated leakage λₙ.

Verification Approach

Leakage contracts enable a two-part verification methodology:

1. Hardware compliance: The processor design (at gate-level/RTL) is verified against the contract, ensuring it does not leak more information than the contract specifies.
2. Software compliance: The masked software implementation is verified against the contract, ensuring it maintains probing security given the leakage the contract permits.

Hardware Verification

Hardware compliance is checked as a 2-safety hyperproperty: for every observable leak in the hardware, there must be a corresponding leak emitted by the contract. This is encoded as an SMT problem with bitvector theories, using the CBMC frontend to encode the contract and the Boolector SMT solver to verify against the CPU circuit encoding.

Software Verification

Software compliance requires the user to provide assembly code and identify secret locations. Verification proceeds in two steps:

1. Record all leakages emitted by executing the program according to the contract's semantics.
2. Prove order-t probing security by showing all combinations of at most t observations are independent from secrets, using Fourier coefficient approximation and modern SAT solvers.

Extensions to Transition and Glitch Leakage

The original leakage contracts (Bloem et al.) considered only transition leakage — leakage from changes between consecutive states. Extended models account for glitch leakage arising from the gate-level implementation of microarchitectural components such as register file read/write ports and memory interfaces.

For example, in the RISC-V Ibex processor, the register file read port uses a one-hot decoder combined with AND/OR gates. Glitches can propagate through this combinational logic, potentially leaking values of registers not used by the current instruction. In the worst case, glitches from the register file or memory read ports can propagate to the write ports.

The extended gate-level leakage model formalizes:

• Signal stability for each CMOS gate type
• Detectable difference for each gate with respect to input values and stability
• Recursive application to the netlist to capture all potentially occurring glitches

This tighter model accounts for scenarios where glitch propagation is terminated (not all glitches propagate through the entire cone of a gate), reducing false positives in leakage analysis.

Contract Modeling for Ibex (RV32E)

The Ibex contract maintains both architectural and leakage registers:

• Architectural state: pc, next_pc, regs (register file x1–x15)
• Leakage registers: prev_regs (previous register file state), mem_last_addr, mem_last_read, prev_rd, prev_rs1, prev_rs2

The step function executes one instruction: sets next_pc = pc + 4, calls execute(op) which extracts the 7-bit opcode and dispatches to the appropriate implementation, then commits pc = next_pc.

Related Tools and DSLs

• Genoa: A DSL introduced by Bloem et al. for specifying leakage contracts.
• scVerif: Used to verify software against contracts (requires manual translation of the leakage model from Genoa to scVerif's DSL).
• Coco: Directly models leakage of every gate in the hardware netlist, covering glitches and transitions but requiring per-program, per-CPU-version verification.
• LeaSyn: A tool for automatically synthesizing sound and precise leakage contracts for RTL processor designs, alternating between contract synthesis (for precision) and contract verification (for soundness), starting from a user-provided contract template.

Challenges

• Soundness vs. precision: A contract must be sound (not over-approximating leaks) and precise (faithfully representing actual leaks). Coming up with such a contract manually requires deep knowledge of microarchitectural timing side channels and is time-consuming and error-prone.
• Synthesis: Automated tools like LeaSyn address this by synthesizing contracts from templates, validated against open-source RISC-V CPUs, producing contracts that are sound and more precise than manually constructed ones.

Case Study: Ibex Processor

The Ibex core (widely used in embedded systems research) has been extensively studied as a case study. Multiple masked implementations of gadgets and ciphers at various masking orders have been verified against Ibex leakage contracts. Results show that the contract-based approach is significantly faster than direct software-against-hardware-netlist verification, since hardware verification is performed only once and reused across all programs.

Related Work

• Wang et al. [WMvG+23] propose a similar notion of leakage contracts aimed at verifying non-interference properties for microarchitectural (software-visible) leaks, rather than power side-channel security focused on glitches and transitions.
• MaskVerif verifies probing security and t-NI/t-SNI notions but requires comprehensive leakage models.
• Empirical approaches (power analysis) provide practical security assurance but require high practical effort and provide less formal guarantees.