Formalizing probabilistic noninterference

Conference paper

Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formalizing probabilistic noninterference. 3rd International Conference on Certified Programs and Proofs (CPP 2013). Melbourne, VIC, Australia 11 - 13 Dec 2013 Springer International Publishing. pp. 259-275
TypeConference paper
TitleFormalizing probabilistic noninterference
AuthorsPopescu, A., Hölzl, J. and Nipkow, T.
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.

Research GroupFoundations of Computing group
Conference3rd International Conference on Certified Programs and Proofs (CPP 2013)
Page range259-275
ISSN0302-9743
ISBN
Hardcover9783319035444
PublisherSpringer International Publishing
Publication dates
Print2013
Publication process dates
Deposited27 Apr 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-03545-1_17

Additional information

Published paper appears in: Certified Programs and Proofs, Volume 8307 of the series Lecture Notes in Computer Science pp 259-275, 2013

Web address (URL)http://dx.doi.org/10.1007/978-3-319-03545-1_17
LanguageEnglish
Book titleCertified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings
Permalink -

https://repository.mdx.ac.uk/item/85201

Log in to edit

Download files

Accepted author manuscript
PROB.pdf

  • 18
    total views
  • 3
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as