Journal Article: Information Flow Noninterference via Slicing

[wasserrab10afp]

Daniel Wasserrab, Information Flow Noninterference via Slicing, Gerwin Klein and Tobias Nipkow and Lawrence Paulson (Ed.), Archive of Formal Proofs, March 2010. Formal proof development

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.

Download

[Link]

BibTeX

@article{wasserrab10afp,
  title = {Information Flow Noninterference via Slicing},
  year = {2010},
  month = mar,
  journal = {Archive of Formal Proofs},
  author = {Daniel Wasserrab},
  editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  note = {Formal proof development},
  url = {http://afp.sf.net/entries/InformationFlowSlicing.shtml},
}

Authors at the institute

Former Staff Member
Dr.-Ing. Daniel Wasserrab

Projects

Project

Quis-Custodiet