Lintent: Towards Security Type-Checking of Android Applications

Abstract : The widespread adoption of Android devices has attracted the attention of a growing computer security audience. Fundamental weaknesses and subtle design flaws of the Android architecture have been identified, studied and fixed, mostly through techniques from data-flow analysis, runtime protection mechanisms, or changes to the operating system. This paper complements this research by developing a framework for the analysis of Android applications based on typing techniques. We introduce a formal calculus for reasoning on the Android inter-component communication API and a type-and-effect system to statically prevent privilege escalation attacks on well-typed components. Drawing on our abstract framework, we develop a prototype implementation of Lintent, a security type-checker for Android applications integrated with the Android Development Tools suite. We finally discuss preliminary experiences with our tool, which highlight real attacks on existing applications.
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01515252
Contributor : Hal Ifip <>
Submitted on : Thursday, April 27, 2017 - 10:46:55 AM
Last modification on : Tuesday, August 6, 2019 - 4:56:22 PM
Long-term archiving on : Friday, July 28, 2017 - 12:37:54 PM

File

978-3-642-38592-6_20_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Michele Bugliesi, Stefano Calzavara, Alvise Spanò. Lintent: Towards Security Type-Checking of Android Applications. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.289-304, ⟨10.1007/978-3-642-38592-6_20⟩. ⟨hal-01515252⟩

Share

Metrics

Record views

102

Files downloads

208