2-safety hyperproperty verification
TechniqueA 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.
First seen 6/26/2026
Last seen 6/26/2026
Evidence 2 chunks
Wiki v1
WIKI
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
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
1 connectionsThey reuse the 2-safety approach to encode hardware compliance properties.
CITATIONS
6 sources6 citations — click to expand
[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