Options
Combining different proof techniques for verifying information flow security
Publikationstyp
Conference Paper
Date Issued
2006-07
Sprache
English
Author(s)
First published in
Number in series
4407 LNCS
Start Page
94
End Page
110
Citation
Lecture Notes in Computer Science 4407 LNCS: 94-110 (2007)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Springer
When giving a program access to secret information, one must ensure that the program does not leak the secrets to untrusted sinks. For reducing the complexity of such an information flow analysis, one can employ compositional proof techniques. In this article, we present a new approach to analyzing information flow security in a compositional manner. Instead of committing to a proof technique at the beginning of a verification, this choice is made during verification with the option of flexibly migrating to another proof technique. Our approach also increases the precision of compositional reasoning in comparison to the traditional approach. We illustrate the advantages in two exemplary security analyses, on the semantic level and on the syntactic level.
DDC Class
004: Informatik