Towards Formally Verified Path ORAM in Coq
summary
Formalization of Path ORAM proceeds from a Python prototype to a Coq/Gallina formalization on GitHub, with the claim of machine-checked proofs of functional correctness (reads return the most recent write) and computational indistinguishability of equal-length access sequences. Work verifies the tree layout, position map and stash invariant but probabilistic stash-size bounds, complexity reasoning, and reuse of randomness/PRG libraries remain unfinished; connecting the proof to high-fidelity RTL is an open engineering challenge.
AI-written summary · about
chapters (14)
- 0:00Start
- 0:34Outline
- 1:22How do we preserve user privacy?
- 10:00Path ORAM Algorithm
- 14:44Functional Correctness
- 15:47Security Property
- 18:07Approach - Python
- 18:53Formalization so far - Work In Progress
- 19:38Writeback() Python vs Gallina
- 20:21Reasoning about complexity
- 20:59Proof Reuse
- 21:42Reasoning with probability
- 22:13Prove higher-fidelity implementation
- 22:51Summary
related talks
15mV-ORAM: A Versatile and Adaptive ORAM Framework with Service Transformation...
16mOblivious Plug&Charge: A Privacy-Preserving EV Charging Scheme based on ORAM
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
06mFormal Verification with the Certora Prover
41mMechanised Proofs of Atom Exhaustion in Erlang
27mProofs of proofs: incremental verifiability from recursion and accumulation
11mFormally Verifying YUL Level Static Analyses and Optimization with Coq
32mFormal Verification Made Easy (and fast!)