{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T02:35:38Z","timestamp":1784342138908,"version":"3.55.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The ever increasing expansion of mobile applications into nearly every aspect of modern life, from banking to healthcare systems, is making their security more important than ever. Modern smartphone operating systems (OS) rely substantially on the permission-based security model to enforce restrictions on the operations that each application can perform. In this paper, we perform an analysis of the permission protocol implemented in Android, a popular OS for smartphones. We propose a formal model of the Android permission protocol in Alloy, and describe a fully automatic analysis that identifies potential flaws in the protocol. A study of real-world Android applications corroborates our finding that the flaws in the Android permission protocol can have severe security implications, in some cases allowing the attacker to bypass the permission checks entirely.<\/jats:p>","DOI":"10.1007\/s00165-017-0445-z","type":"journal-article","created":{"date-parts":[[2017,11,7]],"date-time":"2017-11-07T10:43:21Z","timestamp":1510051401000},"page":"525-544","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":53,"title":["A formal approach for detection of security flaws in the android permission system"],"prefix":"10.1145","volume":"30","author":[{"given":"Hamid","family":"Bagheri","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, University of Nebraska, Lincoln, NE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eunsuk","family":"Kang","sequence":"additional","affiliation":[{"name":"Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sam","family":"Malek","sequence":"additional","affiliation":[{"name":"School of Information and Computer Sciences, University of California, Irvine, Irvine, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Jackson","sequence":"additional","affiliation":[{"name":"Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Armando A Costa G Merlo A (2012) Formal modeling and reasoning about the android security framework. In: Palamidessi C Ryan MD (eds) Trustworthy global computing number 8191 in Lecture Notes in Computer Science. Springer Berlin pp 64\u201381. https:\/\/doi.org\/10.1007\/978-3-642-41157-1_5","DOI":"10.1007\/978-3-642-41157-1_5"},{"key":"e_1_2_1_2_2_2","unstructured":"Andoni A Daniliuc D Khurshid S Marinov D. Evaluating the small scope hypothesis. http:\/\/sdg.csail.mit.edu\/pubs\/2002\/SSH.pdf"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Arzt S Rasthofer S Bodden E Bartel A Klein J Le Traon Y Octeau D McDaniel P (2014) Flowdroid: precise context flow field object-sensitive and lifecycle-aware taint analysis for android apps. In: Proceedings of the 35th annual ACM SIGPLAN conference on programming language design and implementation (PLDI 2014)","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bugliesi M Calzavara S Span\u00f2 A (2013) Lintent: towards security type-checking of android applications. In: Beyer D Boreale M (ed) Formal techniques for distributed systems number 7892 in Lecture Notes in Computer Science. Springer Berlin pp 289\u2013304. https:\/\/doi.org\/10.1007\/978-3-642-38592-6_20","DOI":"10.1007\/978-3-642-38592-6_20"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2016.05.039"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bagheri H Kang E Malek S Jackson D (2015) Detection of design flaws in the android permission protocol through bounded verification. In: Proceedings of the 2015 international symposium on formal methods (FM) volume 9109 of Lecture Notes in Computer Science. Springer Berlin pp 73\u201389","DOI":"10.1007\/978-3-319-19249-9_6"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2419611"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bagheri H Sadeghi A Jabbarvand R Malek S (2016) Practical formal synthesis and automatic enforcement of security policies for android. In: Proceedings of the 46th IEEE\/IFIP international conference on dependable systems and networks (DSN) pp 514\u2013525","DOI":"10.1109\/DSN.2016.53"},{"key":"e_1_2_1_2_9_2","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 MobiSys \u201911 New York NY USA. ACM pp 239\u2013252","DOI":"10.1145\/1999995.2000018"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Chaudhuri A (2009) Language-based security on android. In: Proceedings of programming languages and analysis for security (PLAS\u201909) pp 1\u20137","DOI":"10.1145\/1554339.1554341"},{"key":"e_1_2_1_2_11_2","unstructured":"Chen KZ Johnson NM D\u2019Silva V Dai S MacNamara K Magrino TR Wu EX Rinard M Song DX (2013) Contextual policy enforcement in android applications with permission event graphs. In: NDSS San Diego CA"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Davi L Dmitrienko A Sadeghi A-R Winandy M (2010) Privilege escalation attacks on android. In: Proceedings of the 13th international conference on Information security (ISC).","DOI":"10.1007\/978-3-642-18178-8_30"},{"key":"e_1_2_1_2_13_2","unstructured":"Enck W Gilbert P gon Chun B Cox LP Jung J McDaniel P Sheth AN (2011) Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. In: Proceedings of USENIX OSDI"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Enck W Ongtang W McDaniel P (2009) On lightweight mobile phone application certification. In: Proceedings of the 16th ACM conference on Computer and communications security Chicago IL. ACM pp 235\u2013245","DOI":"10.1145\/1653662.1653691"},{"key":"e_1_2_1_2_15_2","unstructured":"Enck W Octeau D McDaniel P Chaudhuri S (2011) A study of android application security. In: Proceedings of USENIX."},{"key":"e_1_2_1_2_16_2","unstructured":"Enck W Octeau D McDaniel P Chaudhuri S (2011) A study of android application security. In: Proceedings of the 20th USENIX conference on security SEC\u201911 San Francisco CA. USENIX Association pp 21\u201321"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Fragkaki E Bauer L Jia L Swasey D (2012) Modeling and enhancing android\u2019s permission system. In: 17th European symposium on research in computer security (ESORICS) pp 1\u201318","DOI":"10.1007\/978-3-642-33167-1_1"},{"key":"e_1_2_1_2_18_2","unstructured":"Fuchs AP Chaudhuri A Foster JS (2009) Scandroid: Automated security certification of android applications"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Felt AP Chin E Hanna S Song D Wagner D (2011) Android permissions demystified. In: 18th ACM conference on computer and communications security (CCS) pp 627\u2013638","DOI":"10.1145\/2046707.2046779"},{"key":"e_1_2_1_2_20_2","unstructured":"Felt AP Wang HJ Moshchuk A Hanna S Chin E (2011) Permission re-delegation: attacks and defenses. In: 20th USENIX security symposium"},{"key":"e_1_2_1_2_21_2","unstructured":"Google. Android system permissions. http:\/\/developer.android.com\/guide\/topics\/security\/permissions.html"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Grace MC Zhou W Jiang X Sadeghi AR (2012) Unsafe exposure analysis of mobile in-app advertisements. In: Proceedings of the fifth ACM conference on security and privacy in wireless and mobile networks WISEC \u201912 Tucson AZ. ACM pp 101\u2013112","DOI":"10.1145\/2185448.2185464"},{"key":"e_1_2_1_2_23_2","unstructured":"Grace M Zhou Y Wang Z Jiang X (2012) Systematic detection of capability leaks in stock android smartphones. In: Proceedings of the 19th annual symposium on network and distributed system security"},{"key":"e_1_2_1_2_24_2","unstructured":"Grace MC Zhou Y Wang Z Jiang X (2012) Systematic detection of capability leaks in stock android smartphones. In: NDSS San Diego CA"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Hammad M Bagheri H Malek S (2017) Determination and enforcement of least-privilege architecture in android. In: 2017 IEEE international conference on software architecture (ICSA) pp 59\u201368","DOI":"10.1109\/ICSA.2017.18"},{"key":"e_1_2_1_2_26_2","unstructured":"Jackson D (2012) Software abstractions: logic language and analysis 2nd edn. MIT Press Cambridge"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Li L Bartel A Klein J Traon YL (2014) Automatically exploiting potential component leaks in android applications. In: Proceedings of the 13th international conference on trust security and privacy in computing and communications Beijing China pp 388\u2013397","DOI":"10.1109\/TrustCom.2014.50"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Lu L Li Z Wu Z Lee W Jiang G (2012) Chex: statically vetting android apps for component hijacking vulnerabilities. In: Proceedings of the ACM conference on computer and communications security (CCS)","DOI":"10.1145\/2382196.2382223"},{"key":"e_1_2_1_2_29_2","unstructured":"Murphy M (2014) Vulnerabilities with custom permissions. http:\/\/commonsware.com\/blog\/2014\/02\/12\/vulnerabilities-custom-permissions.html"},{"key":"e_1_2_1_2_30_2","unstructured":"Octeau D McDaniel P Jha S Bartel A Bodden E Klein J Traon YL (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 Washington DC"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Pearce P Felt AP Nunez G Wagner D (2012) AdDroid: privilege separation for applications and advertisers in android. In: Proceedings of the 7th ACM symposium on information computer and communications security ASIACCS \u201912 Seoul Republic of Korea. ACM pp 71\u201372","DOI":"10.1145\/2414456.2414498"},{"key":"e_1_2_1_2_32_2","unstructured":"Pandita R Xiao X Yang W Enck W Xie T (2013) Whyper: towards automating risk assessment of mobile applications. In: Proceedings of the 22nd USENIX conference on security SEC\u201913 Berkeley CA USA. USENIX Association pp 527\u2013542"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Rastogi V Chen Y Enck W (2013) AppsPlayground: automatic security analysis of smartphone applications. In: Proceedings of the 3rd ACM conference on data and application security and privacy CODASPY \u201913 San Antonio TX. ACM pp 209\u2013220","DOI":"10.1145\/2435349.2435379"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Ravitch T Creswick ER Tomb A Foltzer A Elliott T Casburn L (2014) Multi-app security analysis with FUSE: statically detecting android app collusion. In: Proceedings of the 4th program protection and reverse engineering workshop PPREW-4 New Orleans LA. ACM pp 4:1\u20134:10","DOI":"10.1145\/2689702.2689705"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2615307"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Smith E Coglio A (2015) Android platform modeling and android app verification in the acl2 theorem prover. In: Proceedings of the 7th international conference on verified software: theories tools and experiments VSTTE\u201915 pp 183\u2013201","DOI":"10.1007\/978-3-319-29613-5_11"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Schmerl B Gennari J Sadeghi A Bagheri H Malek S Camara J Garlan D (2016) Architecture modeling and analysis of security in android systems. In: Software architecture. Springer Cham pp 274\u2013290","DOI":"10.1007\/978-3-319-48992-6_21"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Shin W Kiyomoto S Fukushima K Tanaka T (2010) A formal model to analyze the permission authorization and enforcement in the android framework. In: IEEE International conference on privacy security risk and trust pp 944\u2013951","DOI":"10.1109\/SocialCom.2010.140"},{"key":"e_1_2_1_2_39_2","unstructured":"Schlegel R Zhang K Zhou X Intwala M Kapadia A Wang X (2011) Soundcomber: a stealthy and context-aware sound trojan for smartphones. In: Proceedings of 18th annual network and distributed system security symposium (NDSS)"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Torlak E Chang FS-H Jackson D (2008) Finding minimal unsatisfiable cores of declarative specifications. In: FM 2008: formal methods 15th international symposium on formal methods Turku Finland May 26\u201330 2008 proceedings pp 326\u2013341","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"e_1_2_1_2_41_2","unstructured":"Torlak E Jackson D (2007) Kodkod: a relational model finder. In: Tools and algorithms for the construction and analysis of systems 13th international conference TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2007 Braga Portugal March 24\u2013April 1 2007 Proceedings pp 632\u2013647"},{"key":"e_1_2_1_2_42_2","unstructured":"Woodcock J Davies J (1996) Using Z. Specification refinement and proof. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Wu L Grace M Zhou Y Wu C Jiang X (2013) The impact of vendor customizations on android security. In: Proceedings of the 2013 ACM SIGSAC conference on computer and communications security CCS \u201913 Berlin Germany. ACM pp 623\u2013634","DOI":"10.1145\/2508859.2516728"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Larsen PG Bicarregui J Fitzgerald J (2009) Formal methods: practice and experience. ACM Comput Surv 41(4):19:1\u201319:36","DOI":"10.1145\/1592434.1592436"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0445-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0445-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0445-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0445-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:21:07Z","timestamp":1641486067000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0445-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":44,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,9]]}},"alternative-id":["10.1007\/s00165-017-0445-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0445-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9]]}}}