We present models and soundness results for hybrid information flow, i.e. for mechanisms that enforce noninterference-style security guarantees using a combination of static analysis and dynamic taint tracking. Our analysis has the following characteristics: (i) we formulate hybrid information flow as an end-to-end property, in contrast to disruptive monitors that prematurely terminate or otherwise alter an execution upon detecting a potentially illicit flow; (ii) our security notions capture the increased precision that is gained when static analysis is combined with dynamic enforcement; (iii) we introduce path tracking to incorporate a form of termination-sensitivity, and (iv) develop a novel variant of purely dynamic tracking that ignores indirect flows; (v) our work has been formally verified, by a comprehensive representation in the theorem prover Coq. © Springer-Verlag Berlin Heidelberg 2012.
CITATION STYLE
Beringer, L. (2012). End-to-end multilevel hybrid information flow control. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7705 LNCS, pp. 50–65). https://doi.org/10.1007/978-3-642-35182-2_5
Mendeley helps you to discover research relevant for your work.