Inter-Procedural Information Flow Noninterference via Slicing

Title:	Inter-Procedural Information Flow Noninterference via Slicing
Author:	Daniel Wasserrab
Submission date:	2010-03-23
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. This entry contains the part for inter-procedural slicing. See entry InformationFlowSlicing for the intra-procedural part.
Change history:	[2016-06-10]: The original entry InformationFlowSlicing contained both the inter- and intra-procedural case was split into two for easier maintenance.
BibTeX:	@article{InformationFlowSlicing_Inter-AFP, author = {Daniel Wasserrab}, title = {Inter-Procedural Information Flow Noninterference via Slicing}, journal = {Archive of Formal Proofs}, month = mar, year = 2010, note = {\url{http://isa-afp.org/entries/InformationFlowSlicing_Inter.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	HRB-Slicing
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.