Formalizing probabilistic noninterference

Andrei Popescu, Johannes Hol̈zl, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

9 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationCertified Programs and Proofs - Third International Conference, CPP 2013, Proceedings
Pages259-275
Number of pages17
DOIs
StatePublished - 2013
Event3rd International Conference on Certified Programs and Proofs, CPP 2013 - Melbourne, VIC, Australia
Duration: 11 Dec 201313 Dec 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8307 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Conference on Certified Programs and Proofs, CPP 2013
Country/TerritoryAustralia
CityMelbourne, VIC
Period11/12/1313/12/13

Fingerprint

Dive into the research topics of 'Formalizing probabilistic noninterference'. Together they form a unique fingerprint.

Cite this