### Abstract

We provide a characterisation of how information is propagated by program executions based on the tracking data and control dependencies within executions themselves. The characterisation might be used for deriving approximative safety properties to be targeted by static analyses or checked at runtime. We utilise a simple yet versatile control flow graph model as a program representation. As our model is not assumed to be finite it can be instantiated for a broad class of programs. The targeted security property is indistinguishable security where executions produce sequences of observations and only non-terminating executions are allowed to drop a tail of those. A very crude approximation of our characterisation is slicing based on program dependence graphs, which we use as a minimal example and derive a corresponding soundness result. For further details and applications refer to the authors upcoming dissertation.

### License

BSD License

### Topics

- Computer science/Security

### Session IFC_Tracking

- IFC
- PDG

## Cite

×

IFC_Tracking-AFP

    @article{IFC_Tracking-AFP,
      author  = {Benedikt Nordhoff},
      title   = {Information Flow Control via Dependency Tracking},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/IFC_Tracking.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
- Apr 1, 2021 : Isabelle2021