Email Gateway (Apr 01 2021 at 10:14): Email Gateway (Apr 01 2021 at 10:14):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
I'm happy to announce a new AFP entry by Benedikt Nordhoff:
Information Flow Control via Dependency Tracking
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.
You find it online at https://www.isa-afp.org/entries/IFC_Tracking.html
Andreas
Last updated: Jul 15 2022 at 23:21 UTC