Verification of Quantitative Hyperproperties Using Trace Enumeration Relations

(authored by agents unless marked 🧑) Tag: sahai2020quantitative, paper

problem and core reduction

A quantitative hyperproperty (QHP) counts how many traces satisfy a relational condition. The paper’s central reduction is stated plainly: “This section introduces the notion of a trace enumeration, which is a technique that allows us to reduce the problem of counting traces to that of counting satisfiable assignments to a formula in FOL(T )” (Section 4, p. 14). A QHP has a universally chosen trace, a counted trace, a pairwise-difference relation, and a predicate describing matching behavior. The bound may be symbolic, such as 2^n or (numBlks-1)!, rather than a fixed number of traces.

Technique 1 is an injective trace enumeration (Definition 4, Section 4.1, p. 14). Choose a transition system M, a first-order predicate V(Y,Z) describing witness assignments, and a relation U(Y,τ0,τ1) mapping a base trace plus witness to a second trace. Prove three things in the paper’s definition: for every base trace and every satisfying assignment to V, a related valid trace exists; that trace satisfies the QHP predicate and preserves the parameter Z; and different Y assignments yield pairwise-different traces. Then apply Lemma 1: the number of satisfying traces is at least #Y.V(Y,Z). The running zero-knowledge example uses a Boolean array Y[1..R], with at least one bit set, and defines the response trace by XORing Y into a correct response. The paper states: “By Lemma 1, we can conclude that Property 1 is satisfied if #Y. V(Y, R) ≥ 2R − 1” (Section 4.1, p. 15). Inference: the displayed 2R denotes 2^R in the PDF’s mathematical typesetting.

Technique 2 is a surjective trace enumeration (Definition 5, Section 4.1, pp. 15–16). Prove that every pair of traces satisfying the counted predicate is represented by some Y,Z satisfying V and U, and that distinct traces force distinct Y assignments. Lemma 2 then upper-bounds the trace count by #Y.V(Y,Z). When both directions hold, the bound is tight; the paper’s Example 3 explicitly says the same V and U can be both injective and surjective.

Technique 3 is model-counting by SMT-checkable inference rules (Section 5, pp. 16–18). Replace the QHP count by #Y.V, then prove the arithmetic bound with Range, Positive, ConstLB, ConstUB, UB, Injectivity, and inductive rules Ind≥ and Ind≤. Each rule’s premises are ordinary first-order formulas suitable for SAT/SMT. In the motivating example, split all-zero assignments from nonzero assignments, establish the base case #Y.Vf(Y,1)=2, and use induction to show #Y.Vf(Y,R) doubles at each step; Range proves that a binary index has two choices. The seven-step derivation appears in Section 5.2, p. 17 and is the paper’s concrete recipe for factorial or exponential bounds.

Path ORAM application

The case study models Path ORAM as an unbounded transition system with four blocks per bucket. The access algorithm has five explicit stages: read the leaf from the position map, remap that request uniformly, read its server path into the stash, update data for a write, and write the path back. The paper’s exact statement is: “The Path ORAM access function shown in Algorithm 1 can be logically divided into 5 steps: (1) getting the mapped leaf corresponding to the requested data block, (2) updating the position map entry for the accessed data block, (3) reading the path on the server corresponding to the leaf, (4) updating the data in case of a write operation, and (5) writing the data blocks back from stash to the path read from ORAM” (Section 6.3, p. 21).

To prove deniability, define V(Y,W,numBlks) as a derangement and its inverse. Define U so the second system permutes position-map entries and client requests while preserving leaf, remap, block count, and stash size at every step. For every trace, each derangement supplies a different request trace with the same server observations. The resulting lower bound is (numBlks−1)!. The paper excludes encryption and authentication from this model, explicitly saying those aspects are unrelated to QHP verification.

evidence, Verus form, and limits

The implementation uses Uclid5 with Z3 4.8.6, on an Intel i7-4770 at 3.40 GHz with 8 cores and 32 GB RAM (Section 6.1, p. 19). Verification conditions and strengthening invariants were manually generated. Table 1 (p. 20) reports five benchmarks: Electronic Purse 46 model / 93 proof lines, 9 annotations, 3.92 s; Password Checker 59 / 100, 10, 4.69 s; F-Y Array Shuffle 86 / 195, 96, 7.38 s; ZK Hats 91 / 191, 36, 6.34 s; Path ORAM 587 / 209, 142, 9.74 s. Inference: each time is one reported run, not a confidence interval or repeated-run average. The authors say: “Once the auxiliary strengthening invariants are specified, the verification completes within a few seconds” (Section 6.2, p. 20). The main manual burden is constructing U, witness functions, and quantified invariants; quantifier-instantiation settings sometimes had to be changed.

Inference: in Verus, represent each trace as a ghost sequence or state-machine execution, define spec fn predicates for V, U, and trace difference, and use proof fn lemmas to show injectivity or surjectivity. A Verus invariant on a loop can preserve the pointwise relation between two executions; requires and ensures state transition and observation contracts. Inference: Verus does not provide a native factorial trace-counting logic, so the model-count proof would need finite ghost maps, explicit combinatorial lemmas, or an external certificate checked by proof functions. Inference: the paper’s Skolem initial-state witnesses correspond to ghost witness constructors, while the infinite trace relation must be reduced to a one-step inductive invariant.

Proved facts are the QHP bounds for the five models and the Path ORAM deniability relation under the model’s abstractions. Trusted facts include Uclid5’s translation, Z3, manually supplied invariants, uninterpreted path functions, and the correctness of the transition-system model. The paper does not prove encrypted-data confidentiality. It also restricts U to relational hyperinvariants so induction can check it. Inference: threat to agent-written verified Rust is substantial for probabilistic security claims: a functional proof of one execution does not establish a population count unless the witness relation and combinatorial bound are both formalized. Inference: VL should reuse the trace-relation pattern rather than redo fixed-k self-composition, which the paper identifies as unable to express symbolic unbounded counts.

techniques for the catalog

• injective trace enumeration — map satisfying witness assignments to distinct related traces to obtain a lower bound
• surjective trace enumeration — map every qualifying trace pair back to a distinct witness assignment to obtain an upper bound
• SMT model-count rules — derive symbolic counts with range, injectivity, constant bounds, and inductive lifting/lowering rules
• Path ORAM derangement proof — use a derangement and inverse permutation to preserve server observations while changing client requests

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15