Software Model Checking: A Promising Approach to Verify Mobile App Security: A Position Paper
Authors: 
Irina Măriuca Asăvoae, Hoang Nga Nguyen, Markus Roggenbach, Siraj Ahmed ShaikhAuthors Info & Claims
Article No.: 1, Pages 1 - 2
Abstract
In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion is when, in performing a threat, several apps are working together, i.e., they exchange information which they could not obtain on their own. In this context, we developed the K-Android tool, which provides an encoding of the Android/Smali code semantics within the K framework. K-Android allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems.
References
[1]
Android Open Source Project. 2016. Dalvik Bytecode. https://source.android.com/devices/tech/dalvik/dalvik-bytecode.html. (2016).
[2]
Gilad Arnold, Roman Manevich, Mooly Sagiv, and Ran Shaham. 2006. Combining Shape Analyses by Intersecting Abstractions. In VMCAI2006 (Lecture Notes in Computer Science), Vol. 3855. Springer, 33--48.
[3]
Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. 2014. FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, Edinburgh, United Kingdom - June 09-11, 2014. ACM, 29.
[4]
Irina Mariuca Asavoae, Hoang Nga Nguyen, Markus Roggenbach, and Siraj Ahmed Shaikh. 2016. Utilising K Semantics for Collusion Detection in Android Applications. In FMICS-AVoCS 2016 (Lecture Notes in Computer Science), Vol. 9933. Springer, 142--149.
[5]
Shweta Bhandari, Wafa Ben Jaballah, Vineeta Jain, Vijay Laxmi, Akka Zemmari, Manoj Singh Gaur, and Mauro Conti. 2016. Android App Collusion.reat and Mitigation Techniques. CoRR abs/1611.10076 (2016). h.p://arxiv.org/abs/1611.10076
[6]
Denis Bogdanas and Grigore Rosu. 2015. K-Java: A Complete Semantics of Java. In POPL 2015. ACM, 445--456.
[7]
Kandroid ACID Team. 2017. Kandroid Tool. http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/androidsmali-semantics-k. (2017).
[8]
Johannes Kinder, Florian Zuleger, and Helmut Veith. 2009. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. In VMCAI2009 (Lecture Notes in Computer Science), Vol. 5403. Springer, 214--228.
[9]
Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107--115.
[10]
Florian Martin, Martin Alt, Reinhard Wilhelm, and Christian Ferdinand. 1998. Analysis of Loops. In Compiler Construction, 7th International Conference in ETAPS'98 (Lecture Notes in Computer Science), Vol. 1383. Springer, 80--94.
[11]
Damien Octeau, Daniel Luchaup, Somesh Jha, and Patrick D. McDaniel. 2016. Composite Constant Propagation and its Application to Android Program Analysis. IEEE Trans. Software Eng. 42, 11 (2016), 999--1014.
[12]
Grigore Roşu and Traian Florin Şerbănuţă. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397--434.
Recommendations
From System Services Freezing to System Server Shutdown in Android: All You Need Is a Loop in an App
CCS '15: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications SecurityThe Android OS not only dominates 78.6% of the worldwide smartphone market in 2014, but importantly has been widely used for mission critical tasks (e.g., medical devices, auto/aircraft navigators, embedded in satellite project). The core of Android, ...
Automated detection and mitigation of inter-application security vulnerabilities in Android (invited talk)
DeMobile 2014: Proceedings of the 2nd International Workshop on Software Development Lifecycle for MobileAndroid is the most popular platform for mobile devices. It facilitates sharing data and services between applications by providing a rich inter-application communication system. While such sharing can be controlled by the Android permission system, ...
Studying TLS Usage in Android Apps
CoNEXT '17: Proceedings of the 13th International Conference on emerging Networking EXperiments and TechnologiesTransport Layer Security (TLS), has become the de-facto standard for secure Internet communication. When used correctly, it provides secure data transfer, but used incorrectly, it can leave users vulnerable to attacks while giving them a false sense of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2017
49 pages
ISBN:9781450350983
DOI:10.1145/3103111
Copyright © 2017 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
In-Cooperation
- SIGPLAN: ACM Special Interest Group on Programming Languages
- AITO: Assoc Internationale por les Technologies Objects
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 June 2017
Check for updates
Author Tags
Qualifiers
- Short-paper
- Research
- Refereed limited
Conference
ECOOP '17
Acceptance Rates
FTFJP'17 Paper Acceptance Rate 10 of 12 submissions, 83%;
Overall Acceptance Rate 51 of 75 submissions, 68%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 114Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in