{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:23Z","timestamp":1740099143592,"version":"3.37.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319944593"},{"type":"electronic","value":"9783319944609"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94460-9_16","type":"book-chapter","created":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T11:36:38Z","timestamp":1531136198000},"page":"271-288","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Certified Reference Validation Mechanism for the Permission Model of Android"],"prefix":"10.1007","author":[{"given":"Gustavo","family":"Betarte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan","family":"Campo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felipe","family":"Gorostiaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,10]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, J.P.: Computer Security technology planning study. Technical report, Deputy for Command and Management System, USA (1972)","DOI":"10.21236\/AD0772806"},{"key":"16_CR2","unstructured":"Android Developers: Application Fundamentals. http:\/\/developer.android.com\/guide\/components\/fundamentals.html . Accessed Feb 2018"},{"key":"16_CR3","unstructured":"Android Developers: Requesting Permissions at Run Time. https:\/\/developer.android.com\/intl\/es\/training\/permissions\/requesting.html . Accessed Feb 2018"},{"key":"16_CR4","unstructured":"Android Developers: R.styleable. http:\/\/developer.android.com\/reference\/android\/R.styleable.html . Accessed Feb 2018"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Costa, G., Merlo, A.: Android permissions unleashed. In: Fournet, C., Hicks, M., Vigan\u00f2, L. (eds.) IEEE 28th Computer Security Foundations Symposium, pp. 320\u2013333. IEEE Computer Society (2015)","DOI":"10.1109\/CSF.2015.29"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44659-1_1","volume-title":"Theorem Proving in Higher Order Logics","author":"A Balaa","year":"2000","unstructured":"Balaa, A., Bertot, Y.: Fix-point equations for well-founded recursion in type theory. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 1\u201316. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_1"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11737414_9","volume-title":"Functional and Logic Programming","author":"G Barthe","year":"2006","unstructured":"Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 114\u2013129. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11737414_9"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-03359-9_11","volume-title":"Theorem Proving in Higher Order Logics","author":"S Berghofer","year":"2009","unstructured":"Berghofer, S., Bulwahn, L., Haftmann, F.: Turning inductive into equational specifications. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 131\u2013146. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_11"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-319-25150-9_28","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"G Betarte","year":"2015","unstructured":"Betarte, G., Campo, J.D., Luna, C., Romano, A.: Verifying Android\u2019s permission model. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 485\u2013504. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_28"},{"issue":"1","key":"16_CR10","first-page":"27","volume":"26","author":"G Betarte","year":"2016","unstructured":"Betarte, G., Campo, J.D., Luna, C., Romano, A.: Formal analysis of Android\u2019s permission-based security model. Sci. Ann. Comp. Sci. 26(1), 27\u201368 (2016)","journal-title":"Sci. Ann. Comp. Sci."},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-38592-6_20","volume-title":"Formal Techniques for Distributed Systems","author":"M Bugliesi","year":"2013","unstructured":"Bugliesi, M., Calzavara, S., Span\u00f2, A.: Lintent: towards security type-checking of Android applications. In: Beyer, D., Boreale, M. (eds.) FMOODS\/FORTE 2013. LNCS, vol. 7892, pp. 289\u2013304. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38592-6_20"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-18178-8_29","volume-title":"Information Security","author":"M Conti","year":"2011","unstructured":"Conti, M., Nguyen, V.T.N., Crispo, B.: CRePE: context-related policy enforcement for Android. In: Burmester, M., Tsudik, G., Magliveras, S., Ili\u0107, I. (eds.) ISC 2010. LNCS, vol. 6531, pp. 331\u2013345. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18178-8_29"},{"key":"16_CR13","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.scico.2014.05.017","volume":"95","author":"E Angelis De","year":"2014","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program verification via iterated specialization. Sci. Comput. Program. 95, 149\u2013175 (2014)","journal-title":"Sci. Comput. Program."},{"key":"16_CR14","unstructured":"Felt, A., Wang, H., Moshchuk, A., Hanna, S., Chin, E.: Permission re-delegation: attacks and defenses. In: USENIX Security Symposium. USENIX Association (2011)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-33167-1_1","volume-title":"Computer Security \u2013 ESORICS 2012","author":"E Fragkaki","year":"2012","unstructured":"Fragkaki, E., Bauer, L., Jia, L., Swasey, D.: Modeling and enhancing Android\u2019s permission system. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 1\u201318. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33167-1_1"},{"key":"16_CR16","unstructured":"Gartner: Gartner says worldwide sales of smartphones grew 9 percent in first quarter of 2017. Technical report. Gartner Inc. (2017)"},{"key":"16_CR17","unstructured":"GSI: Formal verification of the security model of Android: Coq code. http:\/\/www.fing.edu.uy\/inco\/grupos\/gsi\/documentos\/proyectos\/Android6-Coq-model.tar.gz . Accessed Feb 2018"},{"key":"16_CR18","unstructured":"Letouzey, P.: Programmation fonctionnelle certifi\u00e9e - L\u2019extraction de programmes dans l\u2019assistant Coq. Ph.D. thesis, Universit\u00e9 Paris-Sud, July 2004"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_12"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Nauman, M., Khan, S., Zhang, X.: Apex: extending android permission model and enforcement with user-defined runtime constraints. In: Proceedings of ASIACCS 2010 (2011)","DOI":"10.1145\/1755688.1755732"},{"key":"16_CR21","unstructured":"Open Handset Alliance: Android project. https:\/\/source.android.com\/ . Accessed Feb 2018"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Shin, W., Kiyomoto, S., Fukushima, K., Tanaka, T.: A formal model to analyze the permission authorization and enforcement in the android framework. In: SocialCom 2010, pp. 944\u2013951. IEEE Computer Society, Washington, DC (2010)","DOI":"10.1109\/SocialCom.2010.140"},{"key":"16_CR23","unstructured":"Shin, W., Kiyomoto, S., Fukushima, K., Tanaka, T.: A first step towards automated permission-enforcement analysis of the android framework. In: SAM 2010, pp. 323\u2013329. CSREA Press (2010)"},{"key":"16_CR24","unstructured":"The Coq Team: The Coq Proof Assistant Reference Manual - Version V8.6 (2016)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-35308-6_9","volume-title":"Certified Programs and Proofs","author":"P-N Tollitte","year":"2012","unstructured":"Tollitte, P.-N., Delahaye, D., Dubois, C.: Producing certified functional code from inductive specifications. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 76\u201391. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_9"},{"key":"16_CR26","volume-title":"Practical Model-Based Testing: A Tools Approach","author":"M Utting","year":"2006","unstructured":"Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann Publishers Inc., San Francisco (2006)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94460-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T10:23:08Z","timestamp":1571566988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94460-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319944593","9783319944609"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94460-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}