Proving Obliviousness of Probabilistic Algorithms with Formal Verification
summary
Claims a practical extension to PSL that supports random-loop conditions and dynamic random choice so probabilistic obliviousness can be proved for algorithms current PSL cannot handle. Demonstrates the target: an oblivious sampling routine whose second phase is uniformly shuffled (akin to Melbourne Shuffle, which gives O(sqrt(n)) versus deterministic O(n log n) alternatives). Implements new sampling rules, a nondeterministic-abstraction strategy, and a semantic extension; formalization in Isabelle ongoing and the plan is to verify the sampling algorithm once complete.
AI-written summary · about
chapters (8)
- 0:00Research plan on obliviousness
- 1:25Memory access side-channels
- 5:16Oblivious algorithms defined
- 7:22Verifying probabilistic obliviousness
- 8:26Challenges in verification
- 13:45Extending PSL for random choices
- 17:58Progress and future plans
- 27:20Q&A
related talks
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
45mAutomated Verification meets Differential Privacy
18mHopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…)
01h 06mOn the Assumptions Used for Obfuscation
54mVerification Dilemmas, Law, and the Promise of Zero-Knowledge Proofs
34mThe Concrete Security of Two-Party Computation: Simple Definitions, and Tight Proofs for PSI and...
01h 06mCompiled Nonlocal Games: From CHSH to BQP Verification
33mObfuscation with Constant Multiplicative Size Overhead