Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference

Andrei Popescu, Johannes Hölzl, Tobias Nipkow

We develop a framework for expressing and analyzing the behavior of probabilistic schedulers. There, we define noninterfering schedulers by a probabilistic interpretation of Goguen and Meseguer's seminal notion of noninterference. Noninterfering schedulers are proved to be safe in the following sense: if a multi-threaded program is possibilistically noninterfering, then it is also probabilistically noninterfering when run under this scheduler.

pdf

BibTeX:

@inproceedings{PopescuHN-CALCO13,
author={Andrei Popescu and Johannes Hölzl and Tobias Nipkow},
title={Noninterfering Schedulers---When Possibilistic Noninterference
       Implies Probabilistic Noninterference},
booktitle={Algebra and Coalgebra in Computer Science (CALCO 2013)},
editor={R. Heckel and S. Milius},
publisher=Springer,series=LNCS,volume={8089},pages={236-252},year=2013}
Isabelle theories in the Archive of Formal Proofs