arrow
Return

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

delete2017-06-01
delete2
PRE
AI
Q
Quoc Huy *
R
Richard Bubel
R
Reiner Hähnle
DOI:10.1016/j.cose.2016.12.002delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

Abstract

En 中文
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. (C) 2016 Elsevier Ltd. All rights reserved.
Keywords:
Test generation
Symbolic execution
Information flow
Declassification
Information erasure
Bug finding

Journal

C
Computers and Security
IF:
5.4
Papers:
4.6K
Citations:
1.4W

Organization

T
Technical University of Darmstadt
Scholars:
1.3W
Papers: 10.0K
Citations: 1.2W