TY - GEN
T1 - Formalizing probabilistic noninterference
AU - Popescu, Andrei
AU - Hol̈zl, Johannes
AU - Nipkow, Tobias
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84893097307&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-03545-1_17
DO - 10.1007/978-3-319-03545-1_17
M3 - Conference contribution
AN - SCOPUS:84893097307
SN - 9783319035444
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 259
EP - 275
BT - Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings
T2 - 3rd International Conference on Certified Programs and Proofs, CPP 2013
Y2 - 11 December 2013 through 13 December 2013
ER -