Hamann, TobiasTobiasHamannHerda, MihaiMihaiHerdaMantel, HeikoHeikoMantelMohr, MartinMartinMohrSchneider, DavidDavidSchneiderTasch, MarkusMarkusTasch2022-10-272022-10-272018-11Lecture Notes in Computer Science 11252 LNCS): 437-453 (2018)http://hdl.handle.net/11420/13843It 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.enInformatikConference Paper10.1007/978-3-030-03638-6_27Other