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 intra-procedural slicing. See entry
InformationFlowSlicing_Inter
for the inter-procedural part.
|
BibTeX: |
@article{InformationFlowSlicing-AFP,
author = {Daniel Wasserrab},
title = {Information Flow Noninterference via Slicing},
journal = {Archive of Formal Proofs},
month = mar,
year = 2010,
note = {\url{http://isa-afp.org/entries/InformationFlowSlicing.html},
Formal proof development},
ISSN = {2150-914x},
}
|