More Web Proxy on the site http://driver.im/

article

CrashSafe: a formal model for proving crash-safety of Android applications

Authors:

Abdullah J. Alzahrani,

Sultan Daud Khan,

Mohammad Alhumaid,

Sultan AbdulazizAuthors Info & Claims

Human-centric Computing and Information Sciences, Volume 8, Issue 1

Article No.: 144, Pages 1 - 24

https://doi.org/10.1186/s13673-018-0144-7

Published: 01 December 2018 Publication History

Abstract

Each software application running on Android powered devices consists of application components that communicate with each other to support application's functionality for enhanced user experience of mobile computing. Application components inside Android system communicate with each other using inter-component communication mechanism based on messages called intents. An android application crashes if it invokes an intent that can not be received by (or resolved to) any application on the device. Application crashes represent a severe fault that relates to compromised users' experience, consequently resulting in decreased ratings, usage trends and revenues for such applications. To address this issue--by formally proving crash-safety property of Android applications--we have defined a formal model of Android inter-component communication using Coq theorem prover. The mathematical model defined in theorem prover allows one to prove the properties of inter-component communication system and check the correctness of the proof in an automated way. To demonstrate the significance of the formal model developed, we carried proof of crash-safety of Android applications using Coq tool. The proposed solution named CrashSafe supports a formal approach that enables one to (i) check the correctness of inter-component communication in Android systems and (ii) establish a formal foundation for other tools to assess Android applications' reliability and safety.

References

[1]

Ahmad W, Kästner C, Sunshine J, Aldrich J (2016) Inter-app communication in android: developer challenges. In: Proceedings of the 13th international conference on mining software repositories. ACM, New York, pp 177---188

Digital Library

[2]

Apple Inc (2017) Apple Apps Store. https://itunes.apple.com/us/genre/ios/id36?mt=8. Accessed June 2017

[3]

Armstrong RC, Punnoose RJ, Wong MH, Mayo JR (2014) Survey of existing tools for formal verification. Tech Rep, Sandia National Laboratories

[4]

Arshad H, Jantan AB, Abiodun OI (2018) Digital forensics: review of issues in scientific validation of digital evidence. J Inf Process Syst 14(2):346---376

[5]

Aydemir B, Charguéraud A, Pierce BC, Pollack R, Weirich S (2008) Engineering formal metatheory. In: Acm sigplan notices, vol 43. ACM, New York, pp 3---15

Digital Library

[6]

Bugiel S, Davi L, Dmitrienko A, Fischer T, Sadeghi AR, Shastry B (2012) Towards taming privilege-escalation attacks on android. In: NDSS, vol 17, p 19

[7]

Bugliesi M, Calzavara S, Spanò A (2013) Lintent: towards security type-checking of android applications. In: Formal techniques for distributed systems. Springer, Berlin, pp 289---304

[8]

Chaudhuri A (2009) Language-based security on android. In: Proceedings of the ACM SIGPLAN fourth workshop on programming languages and analysis for security. ACM, New York, pp 1---7

Digital Library

[9]

Chin E, Felt AP, Greenwood K, Wagner D (2011) Analyzing inter-application communication in android. In: Proceedings of the 9th international conference on Mobile systems, applications, and services. ACM, New York, pp 239---252

Digital Library

[10]

Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT press, Cambridge

Digital Library

[11]

Dietz M, Shekhar S, Pisetsky Y, Shu A, Wallach DS (2011) Quire: lightweight provenance for smart phone operating systems. In: USENIX security symposium, vol 31

Digital Library

[12]

Dinh HT, Lee C, Niyato D, Wang P (2013) A survey of mobile cloud computing: architecture, applications, and approaches. Wireless Commun Mobile Comput 13(18):1587---1611

[13]

Enck W, Ongtang M, McDaniel P (2009) Understanding android security. IEEE Secur Privacy 7(1):50---57

Digital Library

[14]

Faruki P, Bharmal A, Laxmi V, Ganmoor V, Gaur MS, Conti M, Rajarajan M (2015) Android security: a survey of issues, malware penetration, and defenses. IEEE Commun Surv Tutorials 17(2):998---1022

[15]

Felt AP, Chin E, Hanna S, Song D, Wagner D (2011) Android permissions demystified. In: Proceedings of the 18th ACM conference on computer and communications security. ACM, New York, pp 627---638

Digital Library

[16]

Google Inc. Android Apps on Google Play. https://play.google.com/store/apps?hl=en

[17]

Google Inc. Android. https://www.android.com/

[18]

Google Inc (2017) Application fundamentals. https://developer.android.com/guide/components/fundamentals.html. Accessed June 2017

[19]

Google Inc (2017) Intents and intent filters. https://developer.android.com/guide/components/intents-filters.html. Accessed June 2017

[20]

Google Inc (2018) Sending the User to Another App. https://developer.android.com/training/basics/intents/sending.html. Accessed May 2018

[21]

Hall SP, Anderson E (2009) Operating systems for mobile computing. J Comput Sci Coll 25(2):64---71

Digital Library

[22]

INRIA. The Coq Proof Assistant. https://coq.inria.fr/

[23]

Kantola D, Chin E, He W, Wagner D (2012) Reducing attack surfaces for intra-application communication in android. In: Proceedings of the second ACM workshop on security and privacy in smartphones and mobile devices. ACM, New York, pp 69---80

Digital Library

[24]

Khan W, Habib U, Akash A, Khalid S, Sultan Daud K (2017) Coq Script. https://github.com/wilstef/android-ipc. Accessed June 2017

[25]

Kim D (2017) Cloud computing to improve Javascript processing efficiency of mobile applications. J Inf Process Syst 13(4):4

[26]

Li L, Bartel A, Bissyandé TF, Klein J, Le Traon Y, Arzt S, Rasthofer S, Bodden E, Octeau D, McDaniel P (2015) Iccta: detecting inter-component privacy leaks in android apps. In: Proceedings of the 37th international conference on software engineering, vol 1. IEEE Press, pp 280---291

Digital Library

[27]

Maheshwari S (2018) That game on your phone may be tracking what you're watching on tv. https://www.nytimes.com/2017/12/28/business/media/alphonso-app-tracking.html

[28]

Maji AK, Arshad FA, Bagchi S, Rellermeyer JS (2012) An empirical study of the robustness of inter-component communication in android. In: 2012 42nd annual IEEE/IFIP international conference on dependable systems and networks (DSN), pp 1---12

Digital Library

[29]

Meier S, Schmidt B, Cremers C, Basin D (2013) The tamarin prover for the symbolic analysis of security protocols. In: International conference on computer aided verification. Springer, Berlin, pp 696---701

[30]

Moran K, Linares-Vásquez M, Bernal-Cárdenas C, Vendome C, Poshyvanyk D (2017) Crashscope: a practical tool for automated testing of android applications. In: 2017 IEEE/ACM 39th international conference on software engineering companion (ICSE-C), pp 15---18

Digital Library

[31]

Octeau D, Luchaup D, Dering M, Jha S, McDaniel P (2015) Composite constant propagation: application to android inter-component communication analysis. In: Proceedings of the 37th international conference on software engineering, vol 1, IEEE Press, pp. 77---88

Digital Library

[32]

Octeau D, McDaniel P, Jha S, Bartel A, Bodden E, Klein J, Le Traon Y (2013) Effective inter-component communication mapping in android with epicc: an essential step towards holistic security analysis. In: Proceedings of the 22nd USENIX security symposium, pp. 543---558

Digital Library

[33]

Ravindranath L, Nath S, Padhye J, Balakrishnan H (2014) Automatic and scalable fault detection for mobile applications. In: Proceedings of the 12th annual international conference on mobile systems, applications, and services. ACM, New York, pp 190---203

Digital Library

[34]

Sajjad M, Abbasi AA, Malik A, Altamimi AB, Alseadoon IM (2018) Classification and mapping of adaptive security for mobile computing. IEEE Trans Emerg Topics Comput.

[35]

Sasnauskas R, Regehr J (2014) Intent fuzzer: crafting intents of death. In: Proceedings of the 2014 joint international workshop on dynamic analysis (WODA) and software and system performance testing, debugging, and analytics (PERTEA). ACM, New York, pp 1---5

Digital Library

[36]

Satyanarayanan M (2010) Mobile computing: the next decade. In: Proceedings of the 1st ACM workshop on mobile cloud computing & services: social networks and beyond. ACM, New York, p 5

Digital Library

[37]

Schmidt AD, Schmidt HG, Clausen J, Yuksel KA, Kiraz O, Camtepe A, Albayrak S (2008) Enhancing security of linux-based android devices. In: Proceedings of 15th international Linux Kongress. Lehmann

[38]

Shao J, Kuk G, Terrell M, Chen S (2014) Why do applications request my contacts data? a large-scale study on openness and control of user contacts permission in android mobile applicaitons marketplace. Front Bus Res China 8(1):113---135

[39]

The Statistics Portal. Global mobile OS market share 2009---2017, by quarter. https://www.statista.com/statistics/266136/global-market-share-held-by-smartphone-operating-systems/

[40]

Wei F, Roy S, Ou X et al (2014) Amandroid: a precise and general inter-component data flow analysis framework for security vetting of android apps. In: Proceedings of the 2014 ACM SIGSAC conference on computer and communications security. ACM, New York, pp 1329---1341

Digital Library

[41]

Ye H, Cheng S, Zhang L, Jiang F (2013) Droidfuzzer: fuzzing the android apps with intent-filter tag. In: Proceedings of international conference on advances in mobile computing & multimedia. ACM, New York, p 68

Digital Library

Cited By

Cristiá MDe Luca GLuna C(2023)An Automatically Verified Prototype of the Android Permissions SystemJournal of Automated Reasoning10.1007/s10817-023-09666-267:2Online publication date: 12-May-2023
https://dl.acm.org/doi/10.1007/s10817-023-09666-2
Khan WKamran MNaqvi SKhan FAlghamdi AAlsolami EAl-Turjman F(2020)Formal Verification of Hardware Components in Critical SystemsWireless Communications & Mobile Computing10.1155/2020/73467632020Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.1155/2020/7346763
Souri ARahmani ANavimipour NRezaei R(2019)A symbolic model checking approach in formal verification of distributed systemsHuman-centric Computing and Information Sciences10.1186/s13673-019-0165-x9:1(1-27)Online publication date: 1-Dec-2019
https://dl.acm.org/doi/10.1186/s13673-019-0165-x
Show More Cited By

Recommendations

RoppDroid

Android is designed such that Android applications (Apps) can provide functions to each other by providing a complex inter-component communication (ICC) model. While app interactions make it convenient and easy for one app to delegate functionality to ...
Binary compatible graphics support in Android for running iOS apps
Middleware '17: Proceedings of the 18th ACM/IFIP/USENIX Middleware Conference

Mobile apps make extensive use of GPUs on smartphones and tablets to access Web content. To support pervasive Web content, we introduce three key OS techniques for binary graphics compatibility necessary to build a real-world system to run iOS and ...
Cider: native execution of iOS apps on android
ASPLOS '14

We present Cider, an operating system compatibility architecture that can run applications built for different mobile ecosystems, iOS or Android, together on the same smartphone or tablet. Cider enhances the domestic operating system, Android, of a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Human-centric Computing and Information Sciences

Human-centric Computing and Information Sciences Volume 8, Issue 1

December 2018

787 pages

ISSN:2192-1962

EISSN:2192-1962

Issue’s Table of Contents

Copyright © Copyright © 2018 The Author(s).

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 December 2018

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cristiá MDe Luca GLuna C(2023)An Automatically Verified Prototype of the Android Permissions SystemJournal of Automated Reasoning10.1007/s10817-023-09666-267:2Online publication date: 12-May-2023
https://dl.acm.org/doi/10.1007/s10817-023-09666-2
Khan WKamran MNaqvi SKhan FAlghamdi AAlsolami EAl-Turjman F(2020)Formal Verification of Hardware Components in Critical SystemsWireless Communications & Mobile Computing10.1155/2020/73467632020Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.1155/2020/7346763
Souri ARahmani ANavimipour NRezaei R(2019)A symbolic model checking approach in formal verification of distributed systemsHuman-centric Computing and Information Sciences10.1186/s13673-019-0165-x9:1(1-27)Online publication date: 1-Dec-2019
https://dl.acm.org/doi/10.1186/s13673-019-0165-x
Talkington JDantu RMorozov KKerschbaum FMashatan ANiu JLee A(2019)Verifying OAuth Implementations Through Encrypted Network AnalysisProceedings of the 24th ACM Symposium on Access Control Models and Technologies10.1145/3322431.3326449(227-229)Online publication date: 28-May-2019
https://dl.acm.org/doi/10.1145/3322431.3326449

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents