Formal Characterization of Illegal Control Flow in Android System

Author

Graa, Mariem ; Cuppens-Boulahia, Nora ; Cuppens, Frederic ; Cavalli, Ana

Author_Institution

Telecom-Bretagne, Cesson-Sevigne, France

fYear

2013

fDate

2-5 Dec. 2013

Firstpage

293

Lastpage

300

Abstract

The dynamic taint analysis mechanism is used to protect sensitive data in the Android system. But this technique does not detect control flows which can cause an under-tainting problem. This means that some values should be marked as tainted, but are not. The under-tainting problem can be the cause of a failure to detect a leak of sensitive information. To solve this problem, we use a set of formally defined rules that describes the taint propagation. We prove the completeness of these rules. Also, we provide a correct and complete algorithm based on these rules to solve the under-tainting problem.

Keywords

Android (operating system); data privacy; failure analysis; security of data; system monitoring; Android system; dynamic taint analysis mechanism; failure; formal characterization; illegal control flow; leak detection; sensitive data protection; taint propagation; under-tainting problem; Algorithm design and analysis; Connectors; Context; Heuristic algorithms; Security; Smart phones; android system; complete algorithm; control flows; dynamic taint analysis; formal rules; under-tainting;

fLanguage

English

Publisher

ieee

Conference_Titel

Signal-Image Technology & Internet-Based Systems (SITIS), 2013 International Conference on

Conference_Location

Kyoto

Type

conf

DOI

10.1109/SITIS.2013.56

Filename

6727205