Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version)

TL;DR

The paper tackles formal verification of security for probabilistic oblivious algorithms, where attackers observe memory-access patterns. It introduces a logic that unifies classical Hoare reasoning with probabilistic independence within a PSL-based framework, enabling reasoning about dynamic randomness, secret-dependent branches, and random loops. The approach is mechanised in Isabelle/HOL and applied to challenging case studies (Melbourne Shuffle, OlyaSampling, Path ORAM, Path Oblivious Heap), surpassing prior methods. A key contribution is the introduction of certainty and uniform-distribution assertions, plus rules like Unif-Idp and RSample that fuse classical and probabilistic reasoning. The work also uncovers and fixes oversights in PSL, and demonstrates the practical viability of formal verification for secure oblivious systems with negligible failure probabilities via perfect oblivious approximations.

Abstract

We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and invariant needed to verify the security of many practical probabilistic oblivious algorithms. We propose an approach based on reasoning over perfectly oblivious approximations, using a program logic that combines both classical Hoare logic reasoning and probabilistic independence reasoning to support all the needed features. We formalise and prove our new logic sound in Isabelle/HOL and apply our approach to formally verify the security of several challenging case studies beyond the reach of prior methods for proving obliviousness.

Figures (17)

• Figure 1: Verification of the motivating algorithm.
• Figure 2: Programming Language Semantics
• Figure 3: Rules capturing the interplay of classical and probabilistic reasoning.
• Figure 4: Auxiliary Functions for Rules
• Figure 5: Rules inherited from PSL PSL.

Theorems & Definitions (16)

• definition thmcounterdefinition: Expressions
• definition thmcounterdefinition: Atomic assertion semantics
• proposition thmcounterproposition
• definition thmcounterdefinition: Judgement Validity
• definition thmcounterdefinition: Even Partition
• theorem thmcountertheorem
• definition thmcounterdefinition: Supported
• definition thmcounterdefinition: $\epsilon$-Statistical Secrecy
• definition thmcounterdefinition: Obliviousness
• definition thmcounterdefinition: Statistical Distance