Probabilistic Noninterference

Title:	Probabilistic Noninterference
Authors:	Andrei Popescu (a /dot/ popescu /at/ mdx /dot/ ac /dot/ uk) and Johannes Hölzl
Submission date:	2014-03-11
Abstract:	We formalize a probabilistic noninterference for a multi-threaded language with uniform scheduling, where probabilistic behaviour comes from both the scheduler and the individual threads. We define notions probabilistic noninterference in two variants: resumption-based and trace-based. For the resumption-based notions, we prove compositionality w.r.t. the language constructs and establish sound type-system-like syntactic criteria. This is a formalization of the mathematical development presented at CPP 2013 and CALCO 2013. It is the probabilistic variant of the Possibilistic Noninterference AFP entry.
BibTeX:	@article{Probabilistic_Noninterference-AFP, author = {Andrei Popescu and Johannes Hölzl}, title = {Probabilistic Noninterference}, journal = {Archive of Formal Proofs}, month = mar, year = 2014, note = {\url{http://isa-afp.org/entries/Probabilistic_Noninterference.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Coinductive, Markov_Models
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.