A Uniform Information-Flow Security Benchmark Suite for Source Code and Bytecode.

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 RS3 Information-Flow Specification Language, and is open to extensions.