[isabelle] New AFP entry: Information Flow Control via Dependency Tracking



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.