A Uniform Information-Flow Security Benchmark Suite for Source Code and Bytecode
| Autor: | Tobias Hamann, Heiko Mantel, Martin Mohr, David Schneider, Mihai Herda, Markus Tasch |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Source code
Correctness Java Computer science Programming language media_common.quotation_subject 020207 software engineering Java bytecode 02 engineering and technology Specification language computer.software_genre Bytecode Information leakage 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Android (operating system) computer computer.programming_language media_common |
| Zdroj: | Secure IT Systems ISBN: 9783030036379 NordSec |
| Popis: | 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\(^3\) Information-Flow Specification Language, and is open to extensions. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|