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

TL;DR

This paper introduces a new formal verification approach combining classical and probabilistic independence reasoning to verify the security of complex probabilistic oblivious algorithms, overcoming limitations of prior logics.

Contribution

It presents a novel program logic that integrates classical Hoare logic with probabilistic independence reasoning, formalized and proven sound in Isabelle/HOL.

Findings

Successfully verified security of complex oblivious algorithms

Overcame limitations of previous verification methods

Demonstrated applicability on challenging case studies

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.