Skip to content
STIMSMITH

2-safety hyperproperty verification

Technique WIKI v1 · 6/26/2026

A formal verification technique, introduced by Bloem et al. [BGG+22], that checks security-relevant properties of hardware by encoding them as two instances of a hardware design and a leakage contract, unrolled across execution cycles, so that the resulting problem can be discharged with SMT solvers.

2-safety hyperproperty verification

2-safety hyperproperty verification is a formal verification technique used in the setting of leakage-contract-based hardware security analysis. It was introduced by Bloem et al. [BGG+22] and is reused in subsequent work on glitch-aware leakage contracts.

Origin and purpose

The technique was originally proposed to verify that, for every observable leak emitted by a hardware circuit, there is a corresponding leak emitted by a software-level leakage contract that the hardware complies with. The hardware/contract compliance property can be expressed as an SMT problem over bitvector theories [BGG+22], and 2-safety hyperproperty verification is the concrete encoding used to discharge it [1].

How it is encoded

In the leakage-contract verification flow, the verification of each gate modeled by a single leak statement in the contract is performed by:

  1. Encoding the 2-safety hyperproperty as two instances of the hardware and the contract.
  2. Unrolling the hardware for each cycle of the instruction execution.
  3. Issuing an SMT query per combination of gate, cycle, and leak statement [2].

In practice, the SMT encoding of the contract is obtained with the CBMC frontend [CKL04] and checked against the SMT encoding of the CPU circuit using the Boolector SMT solver [NPWB18] [1].

Computational cost

The encoding requires at most one SMT query per combination of gate, cycle, and leak statement [2].

Application to glitch-aware leakage models

2-safety hyperproperty verification is not tied to a single leakage model. It was reused to verify a tighter glitch-propagation model in which leakage is described per CMOS gate through a notion of signal stability and a notion of detectable difference. Applying the detectable-difference notion recursively to a hardware netlist captures potentially occurring glitches, and the resulting security notion is checked using the same 2-safety hyperproperty verification technique [1].

Position in the end-to-end flow

The technique is the hardware-verification step of an end-to-end toolchain in which:

  • Hardware verification (via 2-safety hyperproperty verification and SMT) is performed once.
  • Software verification against the contract is then performed separately, using a Fourier-coefficient-based approximation approach [BGI+18] discharged with modern SAT solvers [1].

This separation is reported to make the overall verification significantly faster than approaches that directly verify software against hardware netlists [1].

LINKED ENTITIES

1 links
Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches USES

CITATIONS

6 sources
6 citations
[1] 2-safety hyperproperty verification was introduced by Bloem et al. [BGG+22] and reused to verify the glitch-aware security notion in the paper. Leakage Contracts for Processors with Transitions and Glitches
[2] Verification of each gate modeled by a single leak statement is performed by encoding the 2-safety hyperproperty as two instances of the hardware and contract and unrolling the hardware for each cycle of the instruction execution. Leakage Contracts for Processors with Transitions and Glitches
[3] The encoding requires at most one SMT query per combination of gate, cycle, and leak statement. Leakage Contracts for Processors with Transitions and Glitches
[4] Hardware compliance verification uses SMT over bitvector theories, with the contract encoded via the CBMC frontend [CKL04] and checked against the CPU circuit encoding using Boolector [NPWB18]. Leakage Contracts for Processors with Transitions and Glitches
[5] The recursive application of a per-gate detectable-difference notion over the netlist, combined with per-gate signal stability, captures potentially occurring glitches, and the resulting security notion is checked using the same 2-safety hyperproperty verification. Leakage Contracts for Processors with Transitions and Glitches
[6] 2-safety hyperproperty verification constitutes the hardware-verification half of an end-to-end toolchain in which software is verified separately against the contract via Fourier-coefficient-based approximation [BGI+18] solved with SAT solvers. Leakage Contracts for Processors with Transitions and Glitches