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

• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• Abstraction, Refinement and Proof for Probabilistic Systems
• Bisimulation through probabilistic testing
• Formal certification of code-based cryptographic proofs
• 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

(10)

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

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)