1. Formal Characterization of Illegal Control Flow in Android System
- Author
-
Ana Cavalli, Nora Cuppens-Boulahia, Mariem Graa, Frédéric Cuppens, Télécom Bretagne (devenu IMT Atlantique), Ex-Bibliothèque, Lab-STICC_TB_CID_SFIIS, Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), Département Logique des Usages, Sciences sociales et Sciences de l'Information (LUSSI), Université européenne de Bretagne - European University of Brittany (UEB)-Télécom Bretagne-Institut Mines-Télécom [Paris] (IMT), Département Logiciels et Réseaux (LOR), and Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP)
- Subjects
[INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] ,Information privacy ,Software_OPERATINGSYSTEMS ,Computer science ,[INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC] ,020207 software engineering ,Data_CODINGANDINFORMATIONTHEORY ,02 engineering and technology ,computer.software_genre ,System monitoring ,Computer security ,[INFO.INFO-ES] Computer Science [cs]/Embedded Systems ,[INFO.INFO-MC]Computer Science [cs]/Mobile Computing ,Information sensitivity ,Control flow ,Taint checking ,[INFO.INFO-MC] Computer Science [cs]/Mobile Computing ,Software_SOFTWAREENGINEERING ,0202 electrical engineering, electronic engineering, information engineering ,[INFO.INFO-ES]Computer Science [cs]/Embedded Systems ,020201 artificial intelligence & image processing ,Data mining ,Android (operating system) ,computer - Abstract
International audience; 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.
- Published
- 2013
- Full Text
- View/download PDF