{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T13:50:31Z","timestamp":1762005031796,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,7,26]],"date-time":"2018-07-26T00:00:00Z","timestamp":1532563200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2018,7,26]],"date-time":"2018-07-26T00:00:00Z","timestamp":1532563200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Hum. Cent. Comput. Inf. Sci."],"published-print":{"date-parts":[[2018,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Each software application running on Android powered devices consists of application components that communicate with each other to support application\u2019s 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\u2019 experience, consequently resulting in decreased ratings, usage trends and revenues for such applications. To address this issue\u2014by formally proving crash-safety property of Android applications\u2014we 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  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\u2019 reliability and safety.<\/jats:p>","DOI":"10.1186\/s13673-018-0144-7","type":"journal-article","created":{"date-parts":[[2018,7,16]],"date-time":"2018-07-16T11:58:08Z","timestamp":1531742288000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["CrashSafe: a formal model for proving crash-safety of Android applications"],"prefix":"10.1186","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0993-5964","authenticated-orcid":false,"given":"Wilayat","family":"Khan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Habib","family":"Ullah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aakash","family":"Ahmad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khalid","family":"Sultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abdullah J.","family":"Alzahrani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sultan Daud","family":"Khan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohammad","family":"Alhumaid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sultan","family":"Abdulaziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,26]]},"reference":[{"key":"144_CR1","doi-asserted-by":"crossref","unstructured":"Ahmad W, K\u00e4stner 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\u2013188","DOI":"10.1145\/2901739.2901762"},{"key":"144_CR2","unstructured":"Apple Inc (2017) Apple Apps Store. https:\/\/itunes.apple.com\/us\/genre\/ios\/id36?mt=8. Accessed June 2017"},{"key":"144_CR3","doi-asserted-by":"crossref","unstructured":"Armstrong RC, Punnoose RJ, Wong MH, Mayo JR (2014) Survey of existing tools for formal verification. Tech Rep, Sandia National Laboratories","DOI":"10.2172\/1166644"},{"issue":"2","key":"144_CR4","first-page":"346","volume":"14","author":"H Arshad","year":"2018","unstructured":"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\u2013376","journal-title":"J Inf Process Syst"},{"key":"144_CR5","doi-asserted-by":"crossref","unstructured":"Aydemir B, Chargu\u00e9raud A, Pierce BC, Pollack R, Weirich S (2008) Engineering formal metatheory. In: Acm sigplan notices, vol\u00a043. ACM, New York, pp 3\u201315","DOI":"10.1145\/1328897.1328443"},{"key":"144_CR6","unstructured":"Bugiel S, Davi L, Dmitrienko A, Fischer T, Sadeghi AR, Shastry B (2012) Towards taming privilege-escalation attacks on android. In: NDSS, vol\u00a017, p\u00a019"},{"key":"144_CR7","doi-asserted-by":"crossref","unstructured":"Bugliesi M, Calzavara S, Span\u00f2 A (2013) Lintent: towards security type-checking of android applications. In: Formal techniques for distributed systems. Springer, Berlin, pp 289\u2013304","DOI":"10.1007\/978-3-642-38592-6_20"},{"key":"144_CR8","doi-asserted-by":"crossref","unstructured":"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\u20137","DOI":"10.1145\/1554339.1554341"},{"key":"144_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013252","DOI":"10.1145\/1999995.2000018"},{"key":"144_CR10","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT press, Cambridge"},{"key":"144_CR11","unstructured":"Dietz M, Shekhar S, Pisetsky Y, Shu A, Wallach DS (2011) Quire: lightweight provenance for smart phone operating systems. In: USENIX security symposium, vol\u00a031"},{"issue":"18","key":"144_CR12","doi-asserted-by":"publisher","first-page":"1587","DOI":"10.1002\/wcm.1203","volume":"13","author":"HT Dinh","year":"2013","unstructured":"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\u20131611","journal-title":"Wireless Commun Mobile Comput"},{"issue":"1","key":"144_CR13","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MSP.2009.26","volume":"7","author":"W Enck","year":"2009","unstructured":"Enck W, Ongtang M, McDaniel P (2009) Understanding android security. IEEE Secur Privacy 7(1):50\u201357","journal-title":"IEEE Secur Privacy"},{"issue":"2","key":"144_CR14","doi-asserted-by":"publisher","first-page":"998","DOI":"10.1109\/COMST.2014.2386139","volume":"17","author":"P Faruki","year":"2015","unstructured":"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\u20131022","journal-title":"IEEE Commun Surv Tutorials"},{"key":"144_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013638","DOI":"10.1145\/2046707.2046779"},{"key":"144_CR16","unstructured":"Google Inc. Android Apps on Google Play. https:\/\/play.google.com\/store\/apps?hl=en"},{"key":"144_CR17","unstructured":"Google Inc. Android. https:\/\/www.android.com\/"},{"key":"144_CR18","unstructured":"Google Inc (2017) Application fundamentals. https:\/\/developer.android.com\/guide\/components\/fundamentals.html. Accessed June 2017"},{"key":"144_CR19","unstructured":"Google Inc (2017) Intents and intent filters. https:\/\/developer.android.com\/guide\/components\/intents-filters.html. Accessed June 2017"},{"key":"144_CR20","unstructured":"Google Inc (2018) Sending the User to Another App. https:\/\/developer.android.com\/training\/basics\/intents\/sending.html. Accessed May 2018"},{"issue":"2","key":"144_CR21","first-page":"64","volume":"25","author":"SP Hall","year":"2009","unstructured":"Hall SP, Anderson E (2009) Operating systems for mobile computing. J Comput Sci Coll 25(2):64\u201371","journal-title":"J Comput Sci Coll"},{"key":"144_CR22","unstructured":"INRIA. The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"144_CR23","doi-asserted-by":"crossref","unstructured":"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\u201380","DOI":"10.1145\/2381934.2381948"},{"key":"144_CR24","unstructured":"Khan W, Habib U, Akash A, Khalid S, Sultan Daud K (2017) Coq Script. https:\/\/github.com\/wilstef\/android-ipc. Accessed June 2017"},{"issue":"4","key":"144_CR25","first-page":"4","volume":"13","author":"D Kim","year":"2017","unstructured":"Kim D (2017) Cloud computing to improve Javascript processing efficiency of mobile applications. J Inf Process Syst 13(4):4","journal-title":"J Inf Process Syst"},{"key":"144_CR26","doi-asserted-by":"crossref","unstructured":"Li L, Bartel A, Bissyand\u00e9 TF, Klein J, Le\u00a0Traon 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\u2013291","DOI":"10.1109\/ICSE.2015.48"},{"key":"144_CR27","unstructured":"Maheshwari S (2018) That game on your phone may be tracking what you\u2019re watching on tv. https:\/\/www.nytimes.com\/2017\/12\/28\/business\/media\/alphonso-app-tracking.html"},{"key":"144_CR28","doi-asserted-by":"crossref","unstructured":"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\u201312","DOI":"10.1109\/DSN.2012.6263963"},{"key":"144_CR29","doi-asserted-by":"crossref","unstructured":"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\u2013701","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"144_CR30","doi-asserted-by":"crossref","unstructured":"Moran K, Linares-V\u00e1squez M, Bernal-C\u00e1rdenas 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\u201318","DOI":"10.1109\/ICSE-C.2017.16"},{"key":"144_CR31","doi-asserted-by":"crossref","unstructured":"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\u201388","DOI":"10.1109\/ICSE.2015.30"},{"key":"144_CR32","unstructured":"Octeau D, McDaniel P, Jha S, Bartel A, Bodden E, Klein J, Le\u00a0Traon 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\u2013558"},{"key":"144_CR33","doi-asserted-by":"crossref","unstructured":"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\u2013203","DOI":"10.1145\/2594368.2594377"},{"key":"144_CR34","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2018.2791459","author":"M Sajjad","year":"2018","unstructured":"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. https:\/\/doi.org\/10.1109\/TETC.2018.2791459","journal-title":"IEEE Trans Emerg Topics Comput"},{"key":"144_CR35","doi-asserted-by":"crossref","unstructured":"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\u20135","DOI":"10.1145\/2632168.2632169"},{"key":"144_CR36","doi-asserted-by":"crossref","unstructured":"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\u00a05","DOI":"10.1145\/1810931.1810936"},{"key":"144_CR37","unstructured":"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"},{"issue":"1","key":"144_CR38","first-page":"113","volume":"8","author":"J Shao","year":"2014","unstructured":"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\u2013135","journal-title":"Front Bus Res China"},{"key":"144_CR39","unstructured":"The Statistics Portal. Global mobile OS market share 2009\u20132017, by quarter. https:\/\/www.statista.com\/statistics\/266136\/global-market-share-held-by-smartphone-operating-systems\/"},{"key":"144_CR40","doi-asserted-by":"crossref","unstructured":"Wei F, Roy S, Ou X et\u00a0al (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\u20131341","DOI":"10.1145\/2660267.2660357"},{"key":"144_CR41","doi-asserted-by":"crossref","unstructured":"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\u00a068","DOI":"10.1145\/2536853.2536881"}],"container-title":["Human-centric Computing and Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13673-018-0144-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s13673-018-0144-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13673-018-0144-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T08:34:49Z","timestamp":1627634089000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1186\/s13673-018-0144-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,26]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["144"],"URL":"https:\/\/doi.org\/10.1186\/s13673-018-0144-7","relation":{},"ISSN":["2192-1962"],"issn-type":[{"type":"electronic","value":"2192-1962"}],"subject":[],"published":{"date-parts":[[2018,7,26]]},"assertion":[{"value":"23 April 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 July 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 July 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"21"}}