A uniform Information-flow security benchmark suite for source code and bytecode

Publikationstyp
Conference Paper
Publikationsdatum
2018-11
Sprache
English
Author
Hamann, Tobias 
Herda, Mihai 
Mantel, Heiko 
Mohr, Martin 
Schneider, David 
Tasch, Markus 
TORE-URI
http://hdl.handle.net/11420/13843
First published in
Lecture notes in computer science 
Number in series
11252 LNCS
Start Page
437
End Page
453
Citation
Lecture Notes in Computer Science 11252 LNCS): 437-453 (2018)
Contribution to Conference
23rd Nordic Conference on Secure IT Systems, NordSec 2018 
Publisher DOI
10.1007/978-3-030-03638-6_27
Scopus ID
2-s2.0-85057405813
Publisher
Springer International Publishing AG
It has become common practice to formally verify the correctness of information-flow analyses wrt. noninterference-like properties. An orthogonal problem is to ensure the correctness of implementations of such analyses. In this article, we propose the benchmark suite IFSpec, which provides sample programs for checking that an information-flow analyzer correctly classifies them as secure or insecure. Our focus is on the Java and Android platforms, and IFSpec supports Java source code, Java bytecode, and Dalvik bytecode. IFSpec is structured into categories that address multiple types of information leakage. We employ IFSpec to validate and compare four information-flow analyzers: Cassandra, Joana, JoDroid, and KeY. IFSpec is based on RIFL, the RS Information-Flow Specification Language, and is open to extensions.
DDC Class
004: Informatik