Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Information Flow Noninterferenc...


view this post on Zulip Email Gateway (Aug 18 2022 at 14:57):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
We are pleased to announce a new entry in the Archive of Formal Proofs [http://afp.sf.net]:

Title:
Information Flow Noninterference via Slicing

Author:
Daniel Wasserrab

Abstract:
In this contribution, we show how correctness proofs for intra- and interprocedural slicing can be used to prove that slicing is able to guarantee information flow noninterference. Moreover, we also illustrate how to lift the control flow graphs of the respective frameworks such that they fulfil the additional assumptions needed in the noninterference proofs. A detailed description of the intraprocedural proof and its interplay with the slicing framework can be found in the PLAS'09 paper by Wasserrab et al.

Cheers,
Gerwin


Last updated: Nov 21 2024 at 12:39 UTC