Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification
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 restricti...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Springer Nature America, Inc
2019
|
| Online Access: | https://hdl.handle.net/1721.1/121239 |
| _version_ | 1826216916014858240 |
|---|---|
| author | Bagheri, Hamid Kang, Eunsuk Jackson, Daniel N. Malek, Sam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Bagheri, Hamid Kang, Eunsuk Jackson, Daniel N. Malek, Sam |
| author_sort | Bagheri, Hamid |
| collection | MIT |
| description | 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. Keywords: Protection Level, Content Provider, Design Flaw, Custom Permission, Alloy Analyzer |
| first_indexed | 2024-09-23T16:55:10Z |
| format | Article |
| id | mit-1721.1/121239 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T16:55:10Z |
| publishDate | 2019 |
| publisher | Springer Nature America, Inc |
| record_format | dspace |
| spelling | mit-1721.1/1212392022-10-03T09:10:03Z Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification Bagheri, Hamid Kang, Eunsuk Jackson, Daniel N. Malek, Sam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science 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. Keywords: Protection Level, Content Provider, Design Flaw, Custom Permission, Alloy Analyzer United States. Defense Advanced Research Projects Agency (Award D11AP00282) United States. National Security Agency (H98230-14-C-0140) United States. Department of Homeland Security (HSHQDC-14-C-B0040) National Science Foundation (U.S.) (CCF-1252644) 2019-06-10T19:16:16Z 2019-06-10T19:16:16Z 2015 2019-05-31T17:16:22Z Article http://purl.org/eprint/type/ConferencePaper 978-3-319-19248-2 978-3-319-19249-9 https://hdl.handle.net/1721.1/121239 Bagheri, Hamid, et al. “Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification.” Proceedings of FM 2015: Formal Methods, edited by Nikolaj Bjørner and Frank de Boer, vol. 9109, Springer International Publishing, 2015, pp. 73–89. en http://dx.doi.org/10.1007/978-3-319-19249-9_6 Proceedings of FM 2015: Formal Methods Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Springer Nature America, Inc MIT web domain |
| spellingShingle | Bagheri, Hamid Kang, Eunsuk Jackson, Daniel N. Malek, Sam Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification |
| title | Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification |
| title_full | Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification |
| title_fullStr | Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification |
| title_full_unstemmed | Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification |
| title_short | Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification |
| title_sort | detection of design flaws in the android permission protocol through bounded verification |
| url | https://hdl.handle.net/1721.1/121239 |
| work_keys_str_mv | AT bagherihamid detectionofdesignflawsintheandroidpermissionprotocolthroughboundedverification AT kangeunsuk detectionofdesignflawsintheandroidpermissionprotocolthroughboundedverification AT jacksondanieln detectionofdesignflawsintheandroidpermissionprotocolthroughboundedverification AT maleksam detectionofdesignflawsintheandroidpermissionprotocolthroughboundedverification |