Formalizing probabilistic noninterference

DOI10.1007/978-3-319-03545-1_17MaRDI QIDQ2938053zbMATH OpenOpenAlexFDO

Authors Andrei Popescu, Johannes Hölzl, Tobias Nipkow

Publication date 13 January 2015

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://eprints.mdx.ac.uk/15369/1/PROB.pdf

Mathematics Subject Classification ID

Theory of programming languages (68N15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formal verification of language-based concurrent noninterference
• Proving concurrent noninterference
• Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference
• scientific article; zbMATH DE number 1330436
• Computational probabilistic non-interference

Cites work

• Abstraction, Refinement and Proof for Probabilistic Systems
• Bisimulation through probabilistic testing
• Formal certification of code-based cryptographic proofs
• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Noninterference for concurrent programs and thread systems
• Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference
• Perspectives of System Informatics
• Practical probability: applying pGCL to lattice scheduling
• Probabilistic guarded commands mechanized in HOL
• Proofs of randomized algorithms in Coq
• Proving concurrent noninterference
• Secure information flow by self-composition
• Theoretical Aspects of Computing – ICTAC 2005
• Verifying pCTL model checking

Cited in

(11)

• A formalized general theory of syntax with bindings
• Markov chains and Markov decision processes in Isabelle/HOL
• A formalized general theory of syntax with bindings: extended version
• Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference
• From operational models to information theory; side channels in pGCL with Isabelle
• Characterizing intransitive noninterference for 3-domain security policies with observability
• Practical probability: applying pGCL to lattice scheduling
• Unwinding Possibilistic Security Properties
• Minimising the probabilistic bisimilarity distance
• Relative security: (dis)proving resilience against semantic optimization vulnerabilities in Isabelle/HOL. Extended version
• Probabilistic Noninterference

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Formalizing probabilistic noninterference

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938053)