Mantel, Heiko ; Sudbrock, Henning ; Krausser, Tina
Puebla, Germán (ed.) (2007):
Combining Different Proof Techniques for Verifying
Information Flow Security.
In: LNCS, 4407, In: 16th International Symposium on Logic Based Program
Synthesis and Transformation, LOPSTR 2006,
Springer, [Conference or Workshop Item]
Abstract
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 approachalso increases the precision of compositional reasoning in comparisonto the traditional approach. We illustrate the advantages in twoexemplary security analyses, on the semantic level and on thesyntactic level.
| Item Type: | Conference or Workshop Item |
|---|---|
| Erschienen: | 2007 |
| Editors: | Puebla, Germán |
| Creators: | Mantel, Heiko ; Sudbrock, Henning ; Krausser, Tina |
| Title: | Combining Different Proof Techniques for Verifying Information Flow Security |
| Language: | ["languages_typename_1" not defined] |
| Abstract: | 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 approachalso increases the precision of compositional reasoning in comparisonto the traditional approach. We illustrate the advantages in twoexemplary security analyses, on the semantic level and on thesyntactic level. |
| Book Title: | 16th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2006 |
| Series: | LNCS |
| Series Volume: | 4407 |
| Publisher: | Springer |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Modeling and Analysis of Information Systems (MAIS) |
| Date Deposited: | 31 Dec 2016 09:57 |
| Identification Number: | mantel.ea:combining:2007 |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum