Glitch-aware leakage model

Overview

The glitch-aware leakage model is a formal hardware leakage model that extends transition-based leakage models to account for transient signal instabilities (glitches) in combinational logic. It was introduced by Haring, Hadžić, and Bloem in their work on closing the gap between software leakage contracts and hardware reality for masked processors. Unlike purely value-based leakage models, the glitch-aware model explicitly reasons about how signal transitions between consecutive cycles can cause intermediate gates to ephemerally take unexpected values, propagating unintended information to observable outputs.

Motivation

Standard transition-based leakage models assume that observable leakage depends only on stable values of registers and combinational signals. However, in real synchronous hardware, signals do not transition instantaneously:

• When a register file read port index switches (e.g., from x1 to x2), individual index bits transition at different times within the same clock cycle.
• One-hot decoder outputs — built from Not and Or gates — therefore become unstable, ephemerally taking the value >.
• The And gates that gate each register's value at the read port output briefly let all registers propagate.
• In the worst case (e.g., switching from x0 to x15 or from x1 to x14), all index bits transition, leaking a combination of the entire register file in a single cycle.

For masked software implementations that intentionally hold multiple shares of the same secret in the register file simultaneously, such an observation lets an adversary combine all shares and break the masking scheme.

Core Predicates

The model is built around two compact per-location predicates that avoid the exponential blow-up of explicitly encoding all transition patterns.

Stability

The stability predicate τg(σi−1, σi, σˆi−1, σˆi) of a location g characterizes whether the gate's contribution to the combined leakage λg(σi−1, σi) ‖ λg(σˆi−1, σˆi) is equivalent to either 𝟙 or 𝟘:

τg(σi−1, σi, σˆi−1, σˆi) := g(σi) = g(σi−1) ∧ g(σˆi) = g(σˆi−1) ∧ g(σi) = g(σˆi)          (10)

Whenever τg evaluates to > or 𝟘, the two hardware leakages are structurally equivalent.

Difference

The difference predicate δg(σi−1, σi, σˆi−1, σˆi) encodes whether the gate's contribution is identical across the two traces:

δg(σi−1, σi, σˆi−1, σˆi) := (g(σi−1) = g(σˆi−1)) ∨ (g(σi) = g(σˆi))                  (13)

This trivially encodes λg(σi−1, σi) = λg(σˆi−1, σˆi).

Gate-Level Stability Rules

The model defines how stability and difference propagate through each gate type:

• Not gates: Negations do not change stability or difference; τc = τa and δc = δa.
• And gates: Stable if either input is stable with value ⊥ (the deactivating value):

  τc := (τa ∧ τb) ∨ (τa ∧ ¬a(σi−1, σi)) ∨ (τb ∧ ¬b(σi−1, σi))                       (11)
  

• Or gates: Same structure as And but with non-negated input terms.
• Xor gates: Stable only if both inputs are 𝟘 or 𝟙:

  τc := τa ∧ τb                                                                       (12)
  

  Difference is inherited from either input.
• Nand, Nor, Xnor: Use the same stability/difference definitions as their non-negated counterparts.

Ibex Instantiation

The model is concretely instantiated for the Ibex RISC-V CPU, which uses one-hot decoders built from Not and Or gates for both register file read ports (selected by rs1, rs2) and the write port (selected by rd). Leakage is emitted in three categories.

Common Leakage

Modeled by the regfile_glitches function, called regardless of instruction. It uses the glitchy_decode helper to determine, via bit-vector arithmetic, which registers will be combined under glitch-induced one-hot instability. For each register, the leak contains either the register value (if the one-hot selector is stable with value >) or 0 (if the selector is ⊥ or stable with > on the wrong register). The combined result is leaked jointly with mem_last_addr, mem_last_read, and the glitchy-decoded values of both read ports in both the current and previous cycle.

Writeback Leakage

The write port uses the same Not/Or one-hot decoding as the read ports. If the one-hot decoding of rd for a register is unstable, the writeback multiplexer emits joint leakage of the writeback value and the register output; if stable with value ⊥, only the register value is leaked. This is modeled by emitting one leak per register that conditionally combines the writeback value with the common leakage.

Load Leakage

Modeled by load_leakage, which is called only for load instructions and accounts for the two-cycle nature of Ibex loads:

• Cycle 1 (request): Common leakage suffices, since the memory response has not yet returned.
• Cycle 2 (response): The CPU is stalled, so most control signals are stable. Only the stable values of rs1, mem_last_addr, and req_data are leaked, combined with writeback leakage for the destination register.

Pruning Glitch Propagation

The number of registers whose values combine at the read port output halves for every stable index bit between consecutive instructions. For example, switching from x2 to x3 causes only two registers to combine, while switching from x3 to x1 preserves the stability of rs1[0] and prevents propagation of x0 through x2. This pruning effect is what enables optimized masked software: as long as the index transition does not touch all bits, only a limited subset of registers is jointly leaked.

Efficient Hardware Verification

Directly encoding the full hardware leakage function λg(σi−1, σi) would produce an encoding whose size is exponential in the number of locations in the gate's cone of influence. The glitch-aware encoding uses only the stability and difference predicates, which suffice to verify hardware compliance — i.e., to show that there exist no two state triples ⟨σ−1, σ0, σ0<⟩ and ⟨σˆ−1, σˆ0, σˆ0<⟩ satisfying the contract transition relation for which λ<(σj<) = λ<(σˆj<) but λ(σi−1, σi) ≠ λ(σˆi−1, σˆi). Proving this non-existence implies the existence of a function fλ mapping contract leaks to hardware leaks, closing the verification gap.

Implementation Artifacts

• glitchy_decode: A bit-vector-arithmetic helper that returns a vector of registers, where each entry contains the register value or 0 depending on whether the corresponding one-hot selector bit is stable under the index transition idx → prev_idx.
• regfile_glitches: The top-level contract leak emitter for Ibex common and writeback leakage, which uses glitchy_decode to compute the leaked values for both read ports and conditionally combines them per register.