TY - GEN
T1 - From coupling relations to mated invariants for checking information flow
AU - Naumann, David A.
PY - 2006
Y1 - 2006
N2 - This paper investigates a technique for using automated program verifiers to check conformance with information flow policy, in particular for programs acting on shared, dynamically allocated mutable heap objects. The technique encompasses rich policies with forms of declassification and supports modular, invariant-based verification of object-oriented programs. The technique is based on the known idea of self-composition, whereby noninterference for a command is reduced to an ordinary partial correctness property of the command sequentially composed with a renamed copy of itself. The first contribution is to extend this technique to encompass heap objects, which is difficult because textual renaming is inapplicable. The second contribution is a systematic means to validate transformations on self-composed programs. Certain transformations are needed for effective use of existing automated program verifiers and they exploit conservative flow inference, e.g., from security type inference. Experiments with the technique using ESC/Java2 and Spec# verifiers are reported.
AB - This paper investigates a technique for using automated program verifiers to check conformance with information flow policy, in particular for programs acting on shared, dynamically allocated mutable heap objects. The technique encompasses rich policies with forms of declassification and supports modular, invariant-based verification of object-oriented programs. The technique is based on the known idea of self-composition, whereby noninterference for a command is reduced to an ordinary partial correctness property of the command sequentially composed with a renamed copy of itself. The first contribution is to extend this technique to encompass heap objects, which is difficult because textual renaming is inapplicable. The second contribution is a systematic means to validate transformations on self-composed programs. Certain transformations are needed for effective use of existing automated program verifiers and they exploit conservative flow inference, e.g., from security type inference. Experiments with the technique using ESC/Java2 and Spec# verifiers are reported.
UR - http://www.scopus.com/inward/record.url?scp=33750232981&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33750232981&partnerID=8YFLogxK
U2 - 10.1007/11863908_18
DO - 10.1007/11863908_18
M3 - Conference contribution
AN - SCOPUS:33750232981
SN - 354044601X
SN - 9783540446019
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 279
EP - 296
BT - Computer Security - ESORICS 2006 - 11th European Symposium on Research in Computer Security, Proceedings
T2 - 11th European Symposium on Research in Computer Security, ESORICS 2006
Y2 - 18 September 2006 through 20 September 2006
ER -