TY - GEN
T1 - End-to-end multilevel hybrid information flow control
AU - Beringer, Lennart
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84872237209&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84872237209&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-35182-2_5
DO - 10.1007/978-3-642-35182-2_5
M3 - Conference contribution
AN - SCOPUS:84872237209
SN - 9783642351815
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 50
EP - 65
BT - Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Proceedings
T2 - 10th Asian Symposium on Programming Languages and Systems, APLAS 2012
Y2 - 11 December 2012 through 13 December 2012
ER -