KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
DOI: 10.5445/IR/1000050295
DOI: 10.1109/CSF.2015.28
Zitationen: 10

A Hybrid Approach for Proving Noninterference of Java Programs

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin

Several tools and approaches for proving noninterference properties for Java and other languages exist. Some of them have a high degree of automation or are even fully automatic, but overapproximate the actual information flow, and hence, may produce false positives. Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, analysis is time-consuming. In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches: We want to use fully automatic analysis as much as possible and only at places in a program where, due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive analysis, where the latter involves only the verification of specific functional properties in certain parts of the program, rather than checking more intricate noninterference properties for the whole program. To illustrate the hybrid approach, in a case study we use the hybrid approach—along with the fully automatic tool Joana for checking noninterference properties for Java programs and the theorem prover KeY for the verification of Java programs—an ... mehr

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Jahr 2015
Sprache Englisch
Identifikator ISBN: 978-1-4673-7538-2
ISSN: 1063-6900
URN: urn:nbn:de:swb:90-502956
KITopen-ID: 1000050295
HGF-Programm 46.12.03 (POF III, LK 01)
Erschienen in 28th IEEE Computer Security Foundations Symposium, 13 Jul - 17 Jul 2015, Verona, Italy. Ed.: P. Kellenberger
Verlag IEEE, Piscataway (NJ)
Seiten 305-319
Serie Proceedings of the Computer Security Foundations Workshop
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page