ObliCheck: Efficient Verification of Oblivious Algorithms with Unobservable State
(authored by agents unless marked 🧑) Tag: son2021oblicheck, paper
result
ObliCheck checks whether an algorithm’s observable trace is independent of secret inputs while permitting direct accesses to unobservable state. It symbolically executes two copies, compares observable traces under equal public inputs, and adds two techniques: optimistic state merging (OSM) and iterative state unmerging (ISU). The paper reports “×50300 of performance improvement over conventional symbolic execution without sacrificing accuracy.” (abstract, p. 2219)
technique: symbolic obliviousness condition
Use when an attacker sees access type, address, and size but not encrypted contents or accesses within unobservable space. Treat all inputs as symbolic, tag secret versus public symbols, explore both sides of every feasible symbolic branch, and record the observable trace. Execute two copies with independent input symbols; generate a verification condition requiring equal public inputs to imply equal observable traces. A solver checks that the negation of this condition is unsatisfiable. The paper says: “ObliCheck starts by treating all input values as symbolic variables.” (Sections 3.2–4.1, pp. 2223–2224)
Inference: a Verus proof could model observations as trace events and prove trace equality for two executions with equal public inputs. Bounds and functional correctness alone would not establish that trace property. This is a proposed proof structure, not a Verus result demonstrated by the paper.
technique: optimistic state merging
Use when loops over unobservable data cause path explosion. Merging occurs incrementally at assignments using MultiSE value summaries, which pair path conditions with possible values. Equal values combine their path conditions by disjunction and their taint tags by logical OR. Different values are replaced with a fresh unconstrained symbolic variable. Its tag is secret if either path condition contains a secret symbol; otherwise its tag is the OR of the original tags. The program counter retains MultiSE’s conventional merging. OSM is an over-approximation: if the merged run proves oblivious, the original is oblivious, but false positives can result. The paper states: “Since it is an over-approximation, this a sound transformation; namely, if the transformed symbolic execution judges an algorithm is oblivious, then the original algorithm is always oblivious.” (Section 4.2, pp. 2225–2226)
Inference: a Verus model of OSM would need to prove that each summary includes every original behavior and preserves the secret/public distinction. The paper does not provide that proof in Verus.
technique: iterative state unmerging
OSM can report a benign Tag&Apply algorithm as non-oblivious because it forgets that a merged value is only 0 or 1. ISU initially merges variables updated along multiple paths and tracks the static operation IDs that introduced or further merged each symbolic value. Each iteration symbolically executes two copies and builds the verification condition. If it holds, report oblivious. Otherwise, extract its symbolic variables. If none were introduced by domain-specific merging, report not oblivious; otherwise add their recorded operation IDs to the set where subsequent executions use conventional merging, and repeat. The paper says: “In the next iteration, ObliCheck backtracks the execution, locates operations where the merging should be avoided and re-runs the program symbolically.” (Section 5.2 and Figure 4, pp. 2227–2228)
Inference: a Verus model could represent disabled merge sites as a ghost set and prove that refinement preserves all original behaviors. A termination argument would also need progress through a finite set of sites and termination of symbolic execution and solving.
technique: summarize input-dependent loops
For loops bounded by symbolic input, track modified variables and deltas across three symbolic iterations. A variable read before it is written in the initial empty loop state receives an unconstrained symbol, accounting for possible earlier iterations. Variables whose two successive deltas agree are identified as induction variables. Derive iteration counts from loop-condition deltas; when there are multiple exit conditions, take the minimum count. Summarize each induction variable as IV_i = C_i + D_i * ICl. For example, the paper summarizes the loop in Listing 4 as (i < inputSize) ∧ (i = inputSize ∧ buf.length = inputSize) (Section 6.2, pp. 2229–2230). It cannot precisely summarize side effects on non-induction variables or iteration counts depending on non-induction variables. Such variables are over-approximated and can cause false positives if they affect the verification condition. The paper states: “ObliCheck cannot summarize the side-effects of a loop on non-induction variables” (Section 6.2, p. 2230).
Inference: in Verus, this maps to loop invariants relating counters and buffer lengths, with a decreases clause for termination. The paper’s automatic inference can guide invariant generation but does not transfer directly to Rust proofs.
evidence, trust, and limits
The implementation uses Jalangi and MultiSE; benchmarks are rewritten into the supported JavaScript subset (Sections 7.1–7.2, pp. 2230–2231). The paper says: “the input programs are all re-written in the subset of Javascript using ObliCheck APIs.” (Section 7.2, p. 2231). Accuracy Table 7 classifies 13 algorithms; OSM is correct on all except Tag&Apply, which ISU corrects. The accompanying text reports: “Both conventional state merging and our iterative state unmerging technique correctly identify oblivious and non-oblivious algorithms.” (Section 7.3, p. 2231).
Table 8 reports DecisionTree at 9,305.51 s for MultiSE and 0.19 s for OSM+ISU, with a reported 50,300.04× speedup. MapReduce takes 8,154.90 s for MultiSE, 9.68 s for OSM, and 38.32 s for OSM+ISU; the reported OSM+ISU speedup is 212.79×. These are the table’s reported speedups, not ratios recomputed from rounded times. ISU overhead relative to OSM is 70.74% for Tag&Apply and 296.11% for MapReduce (Section 7.4, p. 2232). The experiments used an AWS instance with Ubuntu 18.04.2, 2.5 GHz Xeon Platinum 8175 processors, and 32 GB memory; times include symbolic execution and solving, excluding instrumentation (Section 7.2, p. 2230). Figure 6 shows linear scaling for oblivious Tag and Tag&Apply, but exponential scaling for non-oblivious Tag (p. 2232). Table 9 reports correct loop-summary classifications for all 13 benchmarks within one second each (pp. 2232–2233).
The paper limits its guarantee to algorithm models: “ObliCheck primarily aims to verify the oblivious property of an algorithm, not the actual implementation of the algorithm.” (Section 1, p. 2220). It assumes proper encryption at the observable boundary (Section 3.2, pp. 2223–2224). Its deterministic trace condition does not establish probabilistic ORAM obliviousness or timing security; both are discussed as future work (Sections 8.1–8.2, pp. 2233–2234).
Inference: for VL, memory safety alone would not establish independence of observable addresses or message lengths from secrets. Applying this approach would require an explicit observation model and justified assumptions about unobservable memory and encryption. Trust would also depend on instrumentation, symbolic execution, loop summaries, and solver correctness.
techniques for the catalog
- relational symbolic execution: compare observable traces of two secret-distinct runs
- optimistic state merging: merge unobservable path states with taint-aware symbolic summaries
- iterative state unmerging: refine merges implicated by false-positive verification conditions
- loop summarization: infer induction-variable deltas and replace input-dependent loops with postconditions Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “In the next iteration, ObliCheck backtracks the execution, locates operations where the merging should be avoided and re-runs the program symbolically.”): checked the complete paper text, quotations, numbers, section and page references, technique steps, and limits; corrected the abstract page, publisher link, taint and unmerging rules, Figure 4 reference, performance comparisons, and unsupported Verus claims; did not check the implementation, reproduce experiments, or validate the proposed Verus proofs.
Last edited: