{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:41:07Z","timestamp":1743140467847,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031081460"},{"type":"electronic","value":"9783031081477"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08147-7_22","type":"book-chapter","created":{"date-parts":[[2022,6,14]],"date-time":"2022-06-14T16:43:08Z","timestamp":1655224988000},"page":"321-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["$$\\mathbb {K}$$-Smali: An Executable Semantics for\u00a0Program Verification of\u00a0Reversed Android Applications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8563-4736","authenticated-orcid":false,"given":"Marwa","family":"Ziadia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4820-3176","authenticated-orcid":false,"given":"Mohamed","family":"Mejri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3905-9099","authenticated-orcid":false,"given":"Jaouhar","family":"Fattahi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,6,15]]},"reference":[{"key":"22_CR1","unstructured":"Mcafee mobile threat report (2020). https:\/\/www.mcafee.com\/content\/dam\/consumer\/en-us\/docs\/2020-Mobile-Threat-Report.pdf"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Stefanescu, A., Park, D., Yuwen, S., Li, Y., Rosu, G.: Semantics-based program verifiers for all languages. In: Visser, E., Smaragdakis, Y., (eds.), Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, 30 October\u20134 November 2016, pp. 74\u201391. ACM (2016)","DOI":"10.1145\/2983990.2984027"},{"issue":"6","key":"22_CR3","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Rosu","year":"2010","unstructured":"Rosu, G., Serbanuta, T.-F.: An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"3","key":"22_CR4","doi-asserted-by":"publisher","first-page":"130","DOI":"10.3390\/info11030130","volume":"11","author":"M Ziadia","year":"2020","unstructured":"Ziadia, M., Fattahi, J., Mejri, M., Pricop, E.: Smali+: an operational semantics for low-level code generated from reverse engineering android applications. Information 11(3), 130 (2020)","journal-title":"Information"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.scico.2014.02.006","volume":"99","author":"K Bae","year":"2015","unstructured":"Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193\u2013234 (2015)","journal-title":"Sci. Comput. Program."},{"key":"22_CR6","unstructured":"Goranko, V., Rumberg, A.: Temporal logic. In: Zalta, E.N. (ed.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2020 edn. (2020)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Bogdanas, D., Rosu, G.: K-Java: a complete semantics of Java. In: Rajamani, S.K., Walker, D., (eds.), Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 445\u2013456. ACM (2015)","DOI":"10.1145\/2676726.2676982"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/978-3-662-44202-9_23","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"D Filaretti","year":"2014","unstructured":"Filaretti, D., Maffeis, S.: An executable formal semantics of PHP. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 567\u2013592. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_23"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Hathhorn, C., Ellison, C., Rosu, G.: Defining the undefinedness of C. In: Grove, D., Blackburn, S., (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15\u201317 June 2015, pp. 336\u2013345. ACM (2015)","DOI":"10.1145\/2737924.2737979"},{"key":"22_CR10","unstructured":"Rosu, G.: $$\\mathbb{K}$$: a semantic framework for programming languages and formal analysis tools. In: Pretschner, A., Peled, D., Hutzelmann, T., (eds.), Dependable Software Systems Engineering, vol. 50, NATO Science for Peace and Security Series-D: Information and Communication Security, pp. 186\u2013206. IOS Press (2017)"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Rosu, G., Chen, X.: Matching logic: the foundation of the K framework (invited talk). In: Blanchette, J., Hritcu, C., (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, 20\u201321 January 2020, p. 1. ACM (2020)","DOI":"10.1145\/3372885.3378574"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-16310-4_8","volume-title":"Rewriting Logic and Its Applications","author":"TF \u015eerb\u0103nu\u0163\u0103","year":"2010","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: K-Maude: a rewriting based tool for semantics of programming languages. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 104\u2013122. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_8"},{"key":"22_CR14","unstructured":"Chen, K.Z., et al.: Contextual policy enforcement in android applications with permission event graphs. In: 20th Annual Network and Distributed System Security Symposium, NDSS 2013, San Diego, California, USA, 24\u201327 February 2013 (2013)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Alhanahnah, M., et al.: Detecting vulnerable android inter-app communication in dynamically loaded code. In: IEEE INFOCOM 2019 - IEEE Conference on Computer Communications, pp. 550\u2013558, April 2019","DOI":"10.1109\/INFOCOM.2019.8737637"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Jerbi, M., Dagdia, Z.C., Bechikh, S., Said, L.B.: On the use of artificial malicious patterns for android malware detection. Comput. Secur. 92, 101743 (2020)","DOI":"10.1016\/j.cose.2020.101743"},{"key":"22_CR17","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2021.102264","volume":"106","author":"H Gao","year":"2021","unstructured":"Gao, H., Cheng, S., Zhang, W.: Gdroid: android malware detection and classification with graph convolutional network. Comput. Secur. 106, 102264 (2021)","journal-title":"Comput. Secur."},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Bai, G., et al.: Towards model checking android applications. IEEE Trans. Softw. Eng. 44(6), 595\u2013612 (2018)","DOI":"10.1109\/TSE.2017.2697848"},{"key":"22_CR19","unstructured":"Mills, E.: Dog wars app for android is trojanized. https:\/\/www.cnet.com\/news\/dog-wars-app-for-android-is-trojanized\/"},{"key":"22_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems - Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Cham (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Felt, A.P., Chin, E., Hanna, S., Song, D., Wagner, D.A.: Android permissions demystified, pp. 627\u2013638 (2011)","DOI":"10.1145\/2046707.2046779"},{"key":"22_CR22","doi-asserted-by":"crossref","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, New York (2011)","DOI":"10.1145\/1999995.2000018"},{"issue":"6","key":"22_CR23","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/2666356.2594299","volume":"49","author":"S Arzt","year":"2014","unstructured":"Arzt, S., et al.: Flowdroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. SIGPLAN Not. 49(6), 259\u2013269 (2014)","journal-title":"SIGPLAN Not."},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"1563","DOI":"10.1109\/TIFS.2020.3025436","volume":"16","author":"R Feng","year":"2021","unstructured":"Feng, R., Chen, S., Xie, X., Meng, G., Lin, S.-W., Liu, Y.: A performance-sensitive malware detection system using deep learning on mobile devices. IEEE Trans. Inf. Forensics Secur. 16, 1563\u20131578 (2021)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"22_CR25","unstructured":"Kumar, R., et al.: IoTmalware: android IoT malware detection based on deep neural network and blockchain technology. CoRR, abs\/2102.13376 (2021)"},{"key":"22_CR26","doi-asserted-by":"publisher","first-page":"16550","DOI":"10.1109\/ACCESS.2019.2895261","volume":"7","author":"W Khan","year":"2019","unstructured":"Khan, W., Kamran, M., Ahmad, A., Khan, F.A., Derhab, A.: Formal analysis of language-based android security using theorem proving approach. IEEE Access 7, 16550\u201316560 (2019)","journal-title":"IEEE Access"},{"issue":"1","key":"22_CR27","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. Comput. Sci. 26(1), 27\u201368 (2016)","journal-title":"Sci. Ann. Comput. Sci."},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Betarte, G., Campo, J., Cristi\u00e1, M., Gorostiaga, F., Luna, C., Sanz, C.: Towards formal model-based analysis and testing of android\u2019s security mechanisms. In: 2017 XLIII Latin American Computer Conference (CLEI), pp. 1\u201310 (2017)","DOI":"10.1109\/CLEI.2017.8226404"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Payet, E., Spoto, F.: An operational semantics for android activities, pp. 121\u2013132 (2014)","DOI":"10.1145\/2543728.2543748"},{"key":"22_CR30","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.scico.2013.11.037","volume":"92","author":"E Wognsen","year":"2014","unstructured":"Wognsen, E., Karlsen, H., Olesen, M.C., Hansen, R.: Formalisation and analysis of Dalvik bytecode. Sci. Comput. Program. 92, 25\u201355 (2014)","journal-title":"Sci. Comput. Program."},{"key":"22_CR31","unstructured":"Jeon, J., Micinski, K.K.: Symdroid: Symbolic Execution for Dalvik (2012)"},{"issue":"6","key":"22_CR32","doi-asserted-by":"publisher","first-page":"304","DOI":"10.3390\/info11060304","volume":"11","author":"R Casolare","year":"2020","unstructured":"Casolare, R., Martinelli, F., Mercaldo, F., Santone, A.: Android collusion: detecting malicious applications inter-communication through sharedpreferences. Information 11(6), 304 (2020)","journal-title":"Information"},{"key":"22_CR33","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"776","DOI":"10.1007\/978-3-030-44038-1_71","volume-title":"Web, Artificial Intelligence and Network Applications","author":"R Casolare","year":"2020","unstructured":"Casolare, R., Martinelli, F., Mercaldo, F., Nardone, V., Santone, A.: Colluding android apps detection via model checking. In: Barolli, L., Amato, F., Moscato, F., Enokido, T., Takizawa, M. (eds.) WAINA 2020. AISC, vol. 1150, pp. 776\u2013786. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44038-1_71"},{"key":"22_CR34","series-title":"Data Analytics","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-59439-2_3","volume-title":"Data Analytics and Decision Support for Cybersecurity","author":"IM As\u0103voae","year":"2017","unstructured":"As\u0103voae, I.M., Blasco, J., Chen, T.M., Kalutarage, H.K., Muttik, I., Nguyen, H.N., Roggenbach, M., Shaikh, S.A.: Detecting malicious collusion between mobile software applications: the androidTM case. In: Palomares Carrascosa, I., Kalutarage, H.K., Huang, Y. (eds.) Data Analytics and Decision Support for Cybersecurity. DA, pp. 55\u201397. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59439-2_3"},{"key":"22_CR35","unstructured":"Ziadia, M., Mejri, M., Fattahi, J.: Formal and automatic security policy enforcement on android applications by rewriting. In: Fujita, H., P\u00e9rez-Meana, H., (eds.), New Trends in Intelligent Software Methodologies, Tools and Techniques - Proceedings of the 20th International Conference on New Trends in Intelligent Software Methodologies, Tools and Techniques, SoMeT 202, Cancun, Mexico, 21\u201323 September 2021, vol. 337, Frontiers in Artificial Intelligence and Applications, pp. 85\u201398. IOS Press (2021)"},{"key":"22_CR36","unstructured":"Ziadia, M., Mejri, M., Fattahi, J.: K semantics for security policy enforcement on android applications with practical cases. In: EAI CICom 2021, editor, 2nd EAI International Conference on Computational Intelligence and Communications, 18\u201319 November 2021 Versailles, France, EAI CICom 2021 (2021)"}],"container-title":["Lecture Notes in Computer Science","Foundations and Practice of Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08147-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,14]],"date-time":"2022-06-14T16:45:12Z","timestamp":1655225112000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08147-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081460","9783031081477"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08147-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"15 June 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FPS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Foundations and Practice of Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 December 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 December 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fps2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fps-2021.com\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"62","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}