[isabelle] New AFP entry: Information Flow Control via Dependency Tracking
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP entry: Information Flow Control via Dependency Tracking
- From: Andreas Lochbihler <mail at andreas-lochbihler.de>
- Date: Thu, 1 Apr 2021 12:14:26 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.1
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and