KIT | KIT-Bibliothek | Impressum | Datenschutz

Integration of Static and Dynamic Analysis Techniques for Checking Noninterference

Beckert, Bernhard ORCID iD icon; Herda, Mihai; Kirsten, Michael ORCID iD icon; Tyszberowicz, Shmuel


In this article, we present an overview of recent combinations of deductive program verification and automatic test generation on the one hand and static analysis on the other hand, with the goal of checking noninterference. Noninterference is the non-functional property that certain confidential information cannot leak to certain public output, i.e., the confidentiality of that information is always preserved.

We define the noninterference properties that are checked along with the individual approaches that we use in different combinations. In one use case, our framework for checking noninterference employs deductive verification to automatically generate tests for noninterference violations with an improved test coverage. In another use case, the framework provides two combinations of deductive verification with static analysis based on system dependence graphs to prove noninterference, thereby reducing the effort for deductive verification.

Postprint §
DOI: 10.5445/IR/1000127291
Veröffentlicht am 05.12.2021
DOI: 10.1007/978-3-030-64354-6_12
Zitationen: 1
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Buchaufsatz
Publikationsdatum 04.12.2020
Sprache Englisch
Identifikator ISBN: 978-3-030-64353-9
ISSN: 1611-3349
KITopen-ID: 1000127291
Erschienen in Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY. Ed.: W. Ahrendt
Verlag Springer
Seiten 287–312
Serie Lecture Notes in Computer Science ; 12345
Projektinformation KASTEL_SKI (BMBF, 16KIS0843)
Bemerkung zur Veröffentlichung Also part of the Programming and Software Engineering book sub series (LNPSE, volume 12345)
Schlagwörter Information-flow security, Deductive verification, Software testing, Program slicing
Nachgewiesen in Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page