Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Information Flow Control via S...


view this post on Zulip Email Gateway (Feb 13 2024 at 11:55):

From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new contribution, by Pasquale Noce: Information Flow Control via Stateful Intransitive Noninterference in Language IMP

From the abstract:

First, the notion of termination-sensitive information flow security with respect to a level-based interference relation is generalized to that of termination-sensitive information flow correctness with respect to such a correctness policy. Then, a static type system is specified and is proven to be capable of enforcing such policies. Finally, the information flow correctness notion and the static type system introduced here are proven to degenerate to the counterparts formalized in Nipkow and Klein's book in case of a stateless level-based information flow correctness policy.

It is now online at https://www.isa-afp.org/entries/IMP_Noninterference.html

Larry


Last updated: Apr 29 2024 at 01:08 UTC