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. © Springer International Publishing 2013.
CITATION STYLE
Popescu, A., Hol̈zl, J., & Nipkow, T. (2013). Formalizing probabilistic noninterference. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8307 LNCS, pp. 259–275). https://doi.org/10.1007/978-3-319-03545-1_17
Mendeley helps you to discover research relevant for your work.