Email Gateway (Aug 19 2022 at 14:01): Email Gateway (Aug 19 2022 at 14:01):From: Lawrence Paulson <lp15@cam.ac.uk>
Probabilistic Noninterference
Authors: Andrei Popescu and Johannes Hölzl
http://afp.sourceforge.net/entries/Probabilistic_Noninterference.shtml
We formalize a probabilistic noninterference for a multi-threaded language with uniform scheduling, where probabilistic behaviour comes from both the scheduler and the individual threads. We define notions probabilistic noninterference in two variants: resumption-based and trace-based. For the resumption-based notions, we prove compositionality w.r.t. the language constructs and establish sound type-system-like syntactic criteria.
This is a formalization of the mathematical development presented at CPP 2013 and CALCO 2013. It is the probabilistic variant of the Possibilistic Noninterference AFP entry.
Larry Paulson
Last updated: Apr 26 2024 at 16:20 UTC