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: Jan 04 2025 at 20:18 UTC