t-Probing Security

Overview

t-Probing security is a formal security model and proof technique used to argue that a masked implementation of a cryptographic algorithm resists physical side-channel attacks (SCAs) such as power or electromagnetic analysis. The model bounds an adversary's observation capability by a parameter t, representing the maximum number of intermediate variables (probes) the adversary is allowed to observe during a computation. An implementation is said to be t-probing secure if no adversary who observes any set of at most t intermediate values can learn anything about the secret inputs.

The notion is central to the soundness of masking, currently the most prominent SCA countermeasure. In a masked implementation, every sensitive intermediate variable is randomly split into at least t+1 shares, so that any t shares are statistically independent of the secret. Provided the t-probing assumption holds, masking is widely believed to defeat most known SCA attacks when t+1 shares are used.

Background: The Probing Model

In the probing model, the adversary is permitted to place a bounded number of physical "probes" (originally conceived as microprobe needles) on intermediate signals during computation. A circuit or program is t-probing secure if, for every set of t probed intermediate variables, the joint distribution of those variables is independent of every secret input.

Formally, for a masked computation f : (x, p, r) → (y, q, λ), the input is partitioned into:

x: shared secret input values,
p: public values,
r: uniform random values,

and the output into shared secret outputs y, public outputs q, and observed leakage λ. The t-probing property requires that any subset of up to t entries of λ is simulatable from p and r alone, without x.

Two practical variants exist:

t-probing security: as above, the simulator has access only to the public inputs and randomness.
t-(S)NI (Strong Non-Interference) security: an enhanced notion with stricter simulatability conditions, which trades ease of verification for higher randomness requirements.

Role in Masking

Masking aims to satisfy the t-probing security model by splitting every sensitive intermediate value into d ≥ t+1 shares. The classical proof strategy is:

Define the masked computation in terms of share-level gadgets.
Show that no combination of t intermediate shares reveals the secret (the probing lemma).
Conclude security against SCAs whose adversarial power is bounded by t probes or by order-t statistical moments (e.g., differential power analysis).

The assumption underpinning this proof strategy is that the adversary's observation capability is bounded — either by the number of physical probes they can place, or by the statistical order of their analyses.

Relation to Hardware Verification: Leakage Contracts

Recent work uses t-probing security as the formal correctness criterion for verifying that hardware correctly implements masked software. In the leakage-contract approach, a contract is a program written in a C-like language that:

specifies the functional ISA behavior of one instruction, and
explicitly emits, through a special leak(...) primitive, every intermediate value an adversary is allowed to observe.

The contract's leakage trace λ is a list of leaked variables accumulated via small-step operational semantics:

⟨σ, λ, "leak(v1,...,vn);" ρ⟩  ⟶  ⟨σ, λ ∪ ⟨v1(σ) ‖ ... ‖ vn(σ)⟩, ρ⟩

Hardware is then verified to be compliant with the contract via a 2-safety hyperproperty, checked by SMT queries. A Model Reduction theorem guarantees that any leakage an attacker can extract by observing side-channel information during a machine-code execution on compliant hardware is also extractable from the contract's λ. Hence, t-probing security of the software with respect to the contract implies t-probing security of the full hardware/software stack.

In practice, t-probing verification is chosen over the stronger t-(S)NI notion because t-(S)NI implementations trade ease-of-verification for higher randomness requirements.

Glitches and Transitions

A well-known limitation of the classical probing model is that it ignores physical phenomena such as glitches and transitions, which can cause gates to leak combinations of values within a single clock cycle. Hardware-aware extensions of t-probing security therefore augment the leakage function λ to capture:

Transition leakage: the previous and current state values at each gate (g(σ_{i-1}) ‖ g(σ_i)).
Glitch leakage: transient intermediate values produced by gate delays.

A precise encoding makes λ dependent on the gate type θ(g) (e.g., AND, OR, register, input) and on whether input signals can fluctuate. For AND gates, leakage of one input is forwarded only if the other input can attain the controlling value during the cycle. Naive concatenations of previous- and current-state values can over-approximate drastically, producing physically impossible leakage scenarios.

Violations of the t-Probing Assumption

The practical soundness of t-probing security rests on the assumption that adversaries cannot obtain unlimited observations of intermediate values. Two demonstrated attack families have been shown to violate this assumption on masked hardware:

Laser Logic State Imaging (LLSI): a contactless laser-assisted technique that extracts the logical state of all registers in a single measurement, providing an effectively unlimited number of probes. Full-key extraction from masked AES hardware has been demonstrated both when register locations are known (single snapshot) and when they are unknown (multiple snapshots combined with a SAT solver).
Impedance / scattering-parameter analysis (LeakyOhm): a non-invasive RF technique that injects high-frequency signals into the power distribution network and analyzes reflected echoes. Because register contents modulate the die's impedance differently at different frequency points, individual registers can be probed simultaneously and independently. A profiled impedance attack has been shown to recover the secret key of a high-order masked AES implementation from a single trace.

These attacks demonstrate that t-probing security, while a sound and useful proof abstraction, does not capture all physical leakage phenomena. They motivate either strengthening the model (e.g., with glitch/transition leakage) or complementing masking with hiding countermeasures such as those effective against impedance leakage.