Formalizing Probabilistic Noninterference

Abstract. We present an Isabelle formalization of probabilistic noninterference for a multi-threaded language with uniform scheduling. Unlike in previous set-tings from the literature, here probabilistic behavior comes from both the sched-uler and the individual threads, making the language more realistic and the math-ematics more challenging. We study resumption-based and trace-based notions of probabilistic noninterference and their relationship, and also discuss composi-tionality w.r.t. the language constructs and type-system-like syntactic criteria. The formalization uses recent development in the Isabelle probability theory library.