TU Darmstadt / ULB / TUbiblio

Combining Different Proof Techniques for Verifying Information Flow Security

Mantel, Heiko ; Sudbrock, Henning ; Krausser, Tina
Hrsg.: Puebla, Germán (2006)
Combining Different Proof Techniques for Verifying Information Flow Security.
Konferenzveröffentlichung, Bibliographie

Kurzbeschreibung (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.

Typ des Eintrags: Konferenzveröffentlichung
Erschienen: 2006
Herausgeber: Puebla, Germán
Autor(en): Mantel, Heiko ; Sudbrock, Henning ; Krausser, Tina
Art des Eintrags: Bibliographie
Titel: Combining Different Proof Techniques for Verifying Information Flow Security
Sprache: Englisch
Publikationsjahr: 2006
Verlag: Raporta di Ricerca CS-2006-5, Università Ca' Foscari Di Venezia
Buchtitel: In Pre-Proceedings of 16th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2006
Kurzbeschreibung (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.

Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Modellierung und Analyse von Informationssystemen (MAIS)
Hinterlegungsdatum: 31 Dez 2016 09:57
Letzte Änderung: 03 Jun 2018 21:30
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen