{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:36:18Z","timestamp":1761510978121},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642411564"},{"type":"electronic","value":"9783642411571"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41157-1_5","type":"book-chapter","created":{"date-parts":[[2013,9,4]],"date-time":"2013-09-04T14:23:39Z","timestamp":1378304619000},"page":"64-81","source":"Crossref","is-referenced-by-count":18,"title":["Formal Modeling and Reasoning about the Android Security Framework"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Costa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessio","family":"Merlo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Abadi, M., Fournet, C.: Access control based on execution history. In: Proceedings of the 10th Annual Network and Distributed System Security Symposium, pp. 107\u2013121 (2003)"},{"key":"5_CR2","series-title":"IFIP AICT","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-642-30436-1_2","volume-title":"Information Security and Privacy Research","author":"A. Armando","year":"2012","unstructured":"Armando, A., Merlo, A., Migliardi, M., Verderame, L.: Would you mind forking this process? A denial of service attack on Android (and some countermeasures). In: Gritzalis, D., Furnell, S., Theoharidou, M. (eds.) SEC 2012. IFIP AICT, vol.\u00a0376, pp. 13\u201324. Springer, Heidelberg (2012)"},{"issue":"4","key":"5_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.5381\/jot.2009.8.4.a1","volume":"8","author":"M. Bartoletti","year":"2009","unstructured":"Bartoletti, M., Costa, G., Degano, P., Martinelli, F., Zunino, R.: Securing Java with Local Policies. Journal of Object Technology\u00a08(4), 5\u201332 (2009)","journal-title":"Journal of Object Technology"},{"issue":"5","key":"5_CR4","doi-asserted-by":"crossref","first-page":"799","DOI":"10.3233\/JCS-2009-0357","volume":"17","author":"M. Bartoletti","year":"2009","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Planning and verifying service composition. Journal of Computer Security (JCS)\u00a017(5), 799\u2013837 (2009)","journal-title":"Journal of Computer Security (JCS)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-71389-0_4","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Bartoletti","year":"2007","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 32\u201347. Springer, Heidelberg (2007)"},{"issue":"6","key":"5_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1552309.1552313","volume":"31","author":"M. Bartoletti","year":"2009","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.-L., Zunino, R.: Local policies for resource usage analysis. ACM Transactions on Programming Languages and Systems\u00a031(6), 1\u201343 (2009)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR7","unstructured":"Bierman, G.M., Parkinson, M.J., Pitts, A.M.: MJ: An imperative core calculus for Java and Java with effects. Technical report, University of Cambridge (2003)"},{"key":"5_CR8","unstructured":"Bugiel, S., Davi, L., Dmitrienko, A., Fischer, T., Sadeghi, A.-R.: Xmandroid: A new android evolution to mitigate privilege escalation attacks. Technical Report TR-2011-04, Technische Univ. Darmstadt (April 2011)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Burguera, I., Zurutuza, U., Nadjm-Therani, S.: Crowdroid: behavior-based malware detection system for android. In: Proceedings of the 1st ACM Workshop on Security and Privacy in Smartphones and Mobile Devices, SPSM 2011 (2011)","DOI":"10.1145\/2046614.2046619"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1554339.1554341","volume-title":"Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS 2009","author":"A. Chaudhuri","year":"2009","unstructured":"Chaudhuri, A.: Language-based security on Android. In: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS 2009, pp. 1\u20137. ACM, New York (2009)"},{"key":"5_CR11","first-page":"239","volume-title":"Proceedings of the 9th International Conference on Mobile Systems, Applications, and Services, MobiSys 2011","author":"E. Chin","year":"2011","unstructured":"Chin, E., Felt, A.P., Greenwood, K., Wagner, D.: Analyzing inter-application communication in Android. In: Proceedings of the 9th International Conference on Mobile Systems, Applications, and Services, MobiSys 2011, pp. 239\u2013252. ACM, New York (2011)"},{"key":"5_CR12","unstructured":"Android Developers. Security and permissions, http:\/\/developer.android.com\/guide\/topics\/security\/security.html"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Felt, A.P., Chin, E., Hanna, S., Song, D., Wagner, D.: Android permissions demystified. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, pp. 627\u2013638 (2011)","DOI":"10.1145\/2046707.2046779"},{"key":"5_CR14","unstructured":"Fuchs, A.P., Chaudhuri, A., Foster, J.S.: Scandroid: Automated security certification of android applications"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A Minimal Core Calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 132\u2013146 (1999)","DOI":"10.1145\/320385.320395"},{"key":"5_CR16","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1145\/2076732.2076781","volume-title":"Proceedings of the 27th Annual Computer Security Applications Conference, ACSAC 2011","author":"T. Luo","year":"2011","unstructured":"Luo, T., Hao, H., Du, W., Wang, Y., Yin, H.: Attacks on webview in the android system. In: Proceedings of the 27th Annual Computer Security Applications Conference, ACSAC 2011, pp. 343\u2013352. ACM, New York (2011)"},{"key":"5_CR17","first-page":"328","volume-title":"Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security, ASIACCS 2010","author":"M. Nauman","year":"2010","unstructured":"Nauman, M., Khan, S., Zhang, X.: Apex: extending android permission model and enforcement with user-defined runtime constraints. In: Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security, ASIACCS 2010, pp. 328\u2013332. ACM, New York (2010)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Ongtang, M., Mclaughlin, S., Enck, W., Mcdaniel, P.: Semantically rich application-centric security in android. In: ACSAC 2009: Annual Computer Security Applications Conference (2009)","DOI":"10.1109\/ACSAC.2009.39"},{"key":"5_CR19","unstructured":"Schlegel, R., Zhang, K., Zhou, X., Intwala, M., Kapadia, A., Wang, X.: Soundcomber: A Stealthy and Context-Aware Sound Trojan for Smartphones. In: Proceedings of the 18th Annual Network & Distributed System Security Symposium (2011)"},{"issue":"2","key":"5_CR20","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1109\/MSP.2010.2","volume":"8","author":"A. Shabtai","year":"2010","unstructured":"Shabtai, A., Fledel, Y., Kanonov, U., Elovici, Y., Dolev, S., Glezer, C.: Google android: A comprehensive security assessment. IEEE Security Privacy\u00a08(2), 35\u201344 (2010)","journal-title":"IEEE Security Privacy"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"944","DOI":"10.1109\/SocialCom.2010.140","volume-title":"Proceedings of the 2010 IEEE Second International Conference on Social Computing, SOCIALCOM 2010","author":"W. Shin","year":"2010","unstructured":"Shin, W., Kiyomoto, S., Fukushima, K., Tanaka, T.: A Formal Model to Analyze the Permission Authorization and Enforcement in the Android Framework. In: Proceedings of the 2010 IEEE Second International Conference on Social Computing, SOCIALCOM 2010, pp. 944\u2013951. IEEE Computer Society, Washington, DC (2010)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-30477-7_8","volume-title":"Programming Languages and Systems","author":"C. Skalka","year":"2004","unstructured":"Skalka, C., Smith, S.: History effects and verification. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol.\u00a03302, pp. 107\u2013128. Springer, Heidelberg (2004)"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1145\/2133601.2133640","volume-title":"Proceedings of the Second ACM Conference on Data and Application Security and Privacy, CODASPY 2012","author":"W. Zhou","year":"2012","unstructured":"Zhou, W., Zhou, Y., Jiang, X., Ning, P.: Detecting repackaged smartphone applications in third-party android marketplaces. In: Proceedings of the Second ACM Conference on Data and Application Security and Privacy, CODASPY 2012, pp. 317\u2013326. ACM, New York (2012)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-21599-5_7","volume-title":"Trust and Trustworthy Computing","author":"Y. Zhou","year":"2011","unstructured":"Zhou, Y., Zhang, X., Jiang, X., Freeh, V.W.: Taming information-stealing smartphone applications (on android). In: McCune, J.M., Balacheff, B., Perrig, A., Sadeghi, A.-R., Sasse, A., Beres, Y. (eds.) TRUST 2011. LNCS, vol.\u00a06740, pp. 93\u2013107. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41157-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,4]],"date-time":"2023-07-04T09:47:12Z","timestamp":1688464032000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41157-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642411564","9783642411571"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41157-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}