Automatic detection and demonstrator generation for information flow leaks in object-oriented programs

•Automatic detection of information flow (IF) leaks.•Support for IF policies: noninterference, declassification, information erasure.•Generation of demonstrator code for found leaks as JUnit tests.•Approach evaluation using micro benchmarks and a case study about E-Voting. We present a method to gen...

Full description

Saved in:
Bibliographic Details
Published in:Computers & security 2017-06, Vol.67, p.335-349
Main Authors: Do, Quoc Huy, Bubel, Richard, Hähnle, Reiner
Format: Article
Language:English
Subjects:
Automation
Benchmarks
Bug finding
Declassification
Information erasure
Information flow
Object oriented programming
Policies
Symbolic execution
Test generation
Test procedures
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:•Automatic detection of information flow (IF) leaks.•Support for IF policies: noninterference, declassification, information erasure.•Generation of demonstrator code for found leaks as JUnit tests.•Approach evaluation using micro benchmarks and a case study about E-Voting. We present a method to generate automatically exploits for information flow leaks in object-oriented programs. The goal, similar to white-box test generation, is to automatically produce executable, reusable test cases that challenge a given information flow policy with a very high degree of guaranteed coverage. Our approach combines self-composition and symbolic execution to create an insecurity formula for a given program and information flow policy. Satisfiability of this formula signifies the presence of information leaks and permits to use model generation for creating exploits. We support different kinds of information flow policies like noninterference, delimited information release, and information erasure. A prototypic tool implementation for Java programs of our approach is available. It generates exploits in the form of self-contained, executable JUnit tests. We evaluate our method and tool based on a set of micro-benchmarks and a case-study on e-voting.
ISSN:0167-4048
1872-6208
DOI:10.1016/j.cose.2016.12.002