### 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.

### License

BSD License

### History

June 10, 2016
  The original entry InformationFlowSlicing contained both the inter- and intra-procedural case was split into two for easier maintenance.

### Topics

- Computer science/Security

### Session InformationFlowSlicing

- NonInterferenceIntra
- LiftingIntra
- NonInterferenceWhile

### Depends on

- Towards Certified Slicing

### Auto-related entries

- Inter-Procedural Information Flow Noninterference via Slicing
- Monadification, Memoization and Dynamic Programming
- Simple Firewall
- Verification of the UpDown Scheme

## Cite

×

InformationFlowSlicing-AFP

    @article{InformationFlowSlicing-AFP,
      author  = {Daniel Wasserrab},
      title   = {Information Flow Noninterference via Slicing},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2010},
      note    = {\url{https://isa-afp.org/entries/InformationFlowSlicing.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Mar 23, 2010 : Isabelle2009-1