Formalizing Probabilistic Noninterference
We present an Isabelle formalization of probabilistic noninterference
for a multi-threaded language with uniform scheduling. Unlike in
previous settings from the literature, here probabilistic behavior
comes from both the scheduler and the individual threads, making the
language more realistic and the mathematics more challenging. We study
resumption-based and trace-based notions of probabilistic
noninterference and their relationship, and also discuss
compositionality w.r.t. the language constructs and type-system-like
syntactic criteria. The formalization uses recent development in the
Isabelle probability theory library.
pdf
BibTeX:
@inproceedings{PopescuHN-CPP13,
author={Andrei Popescu and Johannes Hölzl and Tobias Nipkow},
title={Formalizing Probabilistic Noninterference},
booktitle={Certified Programs and Proofs (CPP 2013)},
editor={G. Gonthier and M. Norrish},
publisher=Springer,series=LNCS,volume={8307},pages={259-275},year=2013}
Isabelle theories in the
Archive of Formal Proofs