KIT | KIT-Bibliothek | Impressum | Datenschutz

A Hybrid Approach for Proving Noninterference of Java Programs

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard ORCID iD icon; Bruns, Daniel; Kirsten, Michael ORCID iD icon; 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–and the CVJ framework proposed by Küsters, Truderung, and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an e-voting system. ... mehr

Volltext §
DOI: 10.5445/IR/1000126291
Veröffentlicht am 07.12.2020
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Forschungsbericht/Preprint
Publikationsdatum 07.05.2015
Sprache Englisch
Identifikator KITopen-ID: 1000126291
HGF-Programm 46.12.03 (POF III, LK 01) Data Security
Umfang 24 S.
Serie (IACR) Cryptology ePrint Archive ; 2015/438
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Externe Relationen Siehe auch
Schlagwörter language-based security, noninterference, program analysis, code-level cryptographic analysis
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page