From: Tobias Nipkow <nipkow@in.tum.de>
Possibilistic Noninterference
Andrei Popescu and Johannes Hölzl
http://afp.sourceforge.net/entries/Possibilistic_Noninterference.shtml
We formalize a wide variety of Volpano/Smith-style noninterference notions for a
while language with parallel composition. We systematize and classify these
notions according to compositionality w.r.t. the language constructs.
Compositionality yields sound syntactic criteria (a.k.a. type systems) in a
uniform way.
An article http://www21.in.tum.de/~nipkow/pubs/cpp12.html about these proofs is
published in the proceedings of the conference Certified Programs and Proofs 2012
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC