TU Darmstadt / ULB / TUbiblio

Combining Different Proof Techniques for Verifying Information Flow Security

Mantel, Heiko and Sudbrock, Henning and Krausser, Tina
Puebla, Germán (ed.) (2006):
Combining Different Proof Techniques for Verifying Information Flow Security.
In: In Pre-Proceedings of 16th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2006, Raporta di Ricerca CS-2006-5, Università Ca' Foscari Di Venezia, [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 comparison to the traditional approach. We illustrate the advantages in two exemplary security analyses, on the semantic level and on the syntactic level.

Item Type: Conference or Workshop Item
Erschienen: 2006
Editors: Puebla, Germán
Creators: Mantel, Heiko and Sudbrock, Henning and 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 comparison to the traditional approach. We illustrate the advantages in two exemplary security analyses, on the semantic level and on the syntactic level.

Title of Book: In Pre-Proceedings of 16th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2006
Publisher: Raporta di Ricerca CS-2006-5, Università Ca' Foscari Di Venezia
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: heiko-mantel-and-henning-sudbrock-and-tina-krauer:combining-different-proof-techniques-for-verifying-information-flow-security:2006
Export:

Optionen (nur für Redakteure)

View Item View Item