Glitch-aware leakage model

Technique

A formal hardware leakage model that extends transition-based leakage models to capture the effect of glitches (transient instabilities) in combinational logic. Introduced by Haring, Hadžić, and Bloem, it is essential for proving the security of masked software against adversaries who can observe combinational side-channel leakage, particularly through one-hot decoder glitches in register file read/write ports. The model uses compact stability and difference predicates to avoid exponential encodings during hardware verification.

First seen 6/26/2026

Last seen 6/26/2026

Evidence 7 chunks

Wiki v1

WIKI

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.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

3 connections

Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches ← introduces 92% 2e

They propose a tighter model accounting for glitch propagation termination and formally develop it.

glitchy_decode ← implements 86% 2e

Encodes selective propagation of register values under unstable one-hot decoders due to glitches.

regfile_glitches ← implements 80% 2e

Emits leaks combining register values and decoded index transitions to reflect glitchy writeback behavior.

LINKED ENTITIES

3 links

Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches INTRODUCES Extracted graph relationship

glitchy_decode IMPLEMENTS Extracted graph relationship

regfile_glitches IMPLEMENTS Extracted graph relationship

CITATIONS

10 sources

10 citations — click to expand

[1] The stability predicate τg is defined as g(σi) = g(σi−1) ∧ g(σˆi) = g(σˆi−1) ∧ g(σi) = g(σˆi). Leakage Contracts for Processors with Transitions and Glitches

[2] The difference predicate δg is defined as (g(σi−1) = g(σˆi−1)) ∨ (g(σi) = g(σˆi)). Leakage Contracts for Processors with Transitions and Glitches

[3] Not gates do not change stability or difference; And/Or gates are stable if either input is stable with the deactivating value; Xor gates are stable only if both inputs are 𝟘 or 𝟙. Leakage Contracts for Processors with Transitions and Glitches

[4] When a read port index switches, glitches in the one-hot decoder can ephemerally propagate every register value to the read port output, in the worst case combining the entire register file in a single cycle. Leakage Contracts for Processors with Transitions and Glitches

[5] The Ibex contract emits three kinds of leakages: common leakage (regfile_glitches), writeback leakage, and load leakage (load_leakage). Leakage Contracts for Processors with Transitions and Glitches

[6] glitchy_decode uses a bit-vector mask over transitioning index bits to determine which registers are combined under glitch-induced one-hot instability. Leakage Contracts for Processors with Transitions and Glitches

[7] The regfile_glitches function emits one leak per register, conditionally combining writeback leakage with common leakage based on rd transitions. Leakage Contracts for Processors with Transitions and Glitches

[8] Load leakage is split across two cycles: cycle 1 emits common leakage, and cycle 2 leaks the stable values of rs1, mem_last_addr, and req_data combined with writeback leakage. Leakage Contracts for Processors with Transitions and Glitches

[9] Hardware verification uses the stability and difference predicates to prove the non-existence of distinguishing state triples, which suffices to imply the existence of a function mapping contract leaks to hardware leaks. Leakage Contracts for Processors with Transitions and Glitches

[10] Each stable register index bit between consecutive instructions halves the number of unstable one-hot signals and therefore halves the number of registers whose values propagate to the read port output. Leakage Contracts for Processors with Transitions and Glitches