Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference
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