{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T04:35:48Z","timestamp":1780634148518,"version":"3.54.1"},"reference-count":43,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2020,2,27]],"date-time":"2020-02-27T00:00:00Z","timestamp":1582761600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information"],"abstract":"<jats:p>Today, Android accounts for more than 80% of the global market share. Such a high rate makes Android applications an important topic that raises serious questions about its security, privacy, misbehavior and correctness. Application code analysis is obviously the most appropriate and natural means to address these issues. However, no analysis could be led with confidence in the absence of a solid formal foundation. In this paper, we propose a full-fledged formal approach to build the operational semantics of a given Android application by reverse-engineering its assembler-type code, called Smali. We call the new formal language Smali     +    . Its semantics consist of two parts. The first one models a single-threaded program, in which a set of main instructions is presented. The second one presents the semantics of a multi-threaded program which is an important feature in Android that has been glossed over in the-state-of-the-art works. All multi-threading essentials such as scheduling, threads communication and synchronization are considered in these semantics. The resulting semantics, forming Smali     +    , are intended to provide a formal basis for developing security enforcement, analysis and misbehaving detection techniques for Android applications.<\/jats:p>","DOI":"10.3390\/info11030130","type":"journal-article","created":{"date-parts":[[2020,2,28]],"date-time":"2020-02-28T09:30:36Z","timestamp":1582882236000},"page":"130","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Smali+: An Operational Semantics for Low-Level Code Generated from Reverse Engineering Android Applications"],"prefix":"10.3390","volume":"11","author":[{"given":"Marwa","family":"Ziadia","sequence":"first","affiliation":[{"name":"Department of Computer Science and Software Engineering, Laval University, Pavillon Adrien-Pouliot 1065, avenue de la M\u00e9decine, Quebec City, QC G1V 0A6, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3905-9099","authenticated-orcid":false,"given":"Jaouhar","family":"Fattahi","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Software Engineering, Laval University, Pavillon Adrien-Pouliot 1065, avenue de la M\u00e9decine, Quebec City, QC G1V 0A6, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohamed","family":"Mejri","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Software Engineering, Laval University, Pavillon Adrien-Pouliot 1065, avenue de la M\u00e9decine, Quebec City, QC G1V 0A6, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4021-6549","authenticated-orcid":false,"given":"Emil","family":"Pricop","sequence":"additional","affiliation":[{"name":"Automatic Control, Computers and Electronics Department. Petroleum-Gas University of Ploiesti, 100680 Ploiesti, Romania"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2020,2,27]]},"reference":[{"key":"ref_1","unstructured":"IDC Corporation (2020, February 19). Smartphone Market Share. Available online: https:\/\/www.idc.com\/promo\/smartphone-market-share\/os."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Zhou, Y., and Jiang, X. (2012, January 20\u201323). Dissecting Android Malware: Characterization and Evolution. Proceedings of the 2012 IEEE Symposium on Security and Privacy, San Francisco, CA, USA.","DOI":"10.1109\/SP.2012.16"},{"key":"ref_3","unstructured":"Sergiu, G. (2020, February 20). Anubis Android Trojan Spotted with Almost Functional Ransomware Module. Available online: https:\/\/www.bleepingcomputer.com\/news\/security\/anubis-android-trojan-spotted-with-almost-functional-ransomware-module\/."},{"key":"ref_4","unstructured":"Barrett, L. (2020, January 02). SMS-Sending Trojan Targets Android Smartphones. Available online: https:\/\/www.esecurityplanet.com\/trends\/article.php\/3898041\/SMSSending-Trojan-Targets-Android-Smartphones.htm\/."},{"key":"ref_5","unstructured":"Collier, N. (2020, January 02). New Android Trojan Malware Discovered in Google Play. Available online: https:\/\/blog.malwarebytes.com\/cybercrime\/2017\/11\/new-trojan-malware-discovered-google-play\/\/."},{"key":"ref_6","unstructured":"F-Secure (2020, January 02). Trojan:Android\/GGTracker. Available online: https:\/\/www.f-secure.com\/v-descs\/trojan_android_ggtracker.shtml."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1145\/2666356.2594299","article-title":"FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps","volume":"49","author":"Arzt","year":"2014","journal-title":"SIGPLAN Not."},{"key":"ref_8","unstructured":"Felt, A.P., Chin, E., Hanna, S., Song, D., and Wagner, D. (, January October). Android Permissions Demystified. Proceedings of the 18th ACM Conference on Computer and Communications Security, New York, NY, USA."},{"key":"ref_9","unstructured":"Davis, B., Sanders, B., Khodaverdian, A., and Chen, H. (, January May). I-arm-droid: A rewriting framework for in-app reference monitors for android applications. Proceedings of the Mobile Security Technologies 2012, San Francisco, CA, USA. Available online: http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.298.7191&rep=rep1&type=pdf."},{"key":"ref_10","unstructured":"Xu, R., Sa\u00efdi, H., and Anderson, R.J. (2012, January 8\u201310). Aurasium: Practical Policy Enforcement for Android Applications. Proceedings of the 21th USENIX Security Symposium, Bellevue, WA, USA."},{"key":"ref_11","unstructured":"Jeon, J., and Micinski, K.K. (2012). SymDroid: Symbolic Execution for Dalvik, University of Maryland. Available online: http:\/\/www.cs.tufts.edu\/~jfoster\/papers\/symdroid.pdf."},{"key":"ref_12","unstructured":"Apktool (2019, February 19). A Tool for Reverse Engineering Android Apk Files. Available online: https:\/\/ibotpeaches.github.io\/Apktool\/."},{"key":"ref_13","first-page":"27","article-title":"Comparative Analysis of Mobile App Reverse Engineering Methods on Dalvik and ART","volume":"6","author":"Na","year":"2016","journal-title":"J. Internet Serv. Inf. Secur."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"El-Zawawy, M.A. (2016, January 4\u20137). An Operational Semantics for Android Applications. Proceedings of the Computational Science and Its Applications - ICCSA 2016 - 16th International Conference, Beijing, China.","DOI":"10.1007\/978-3-319-42092-9_9"},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Payet, E., and Spoto, F. (2019, December 05). An Operational Semantics for Android Activities. Available online: https:\/\/doi.org\/10.1145\/2543728.2543738.","DOI":"10.1145\/2543728.2543738"},{"key":"ref_16","unstructured":"Wognsen, E., and Karlsen, S. (2012). Static Analysis of Dalvik Bytecode and Reflection in Android. [Master\u2019s Thesis, Department of Computer Science Aalborg University]. Available online: https:\/\/projekter.aau.dk\/projekter\/files\/63640573\/rapport.pdf."},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/j.scico.2013.11.037","article-title":"Formalisation and analysis of Dalvik bytecode","volume":"92","author":"Wognsen","year":"2014","journal-title":"Sci. Comput. Program."},{"key":"ref_18","unstructured":"Cousot, P., and Cousot, R. (, January January). Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, New York, NY, USA."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"1192","DOI":"10.1016\/j.infsof.2012.05.003","article-title":"Static Analysis of Android Programs","volume":"54","author":"Payet","year":"2012","journal-title":"Inf. Softw. Technol."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Gunadi, H. (2015, January 9\u201312). Formal Certification of Non-interferent Android Bytecode (DEX Bytecode). Proceedings of the 2015 20th International Conference on Engineering of Complex Computer Systems ICECCS, Gold Coast, Australia.","DOI":"10.1109\/ICECCS.2015.36"},{"key":"ref_21","unstructured":"Gunadi, H., Tiu, A., and Gore, R. (2015). Formal Certification of Android Bytecode. arXiv, Available online: https:\/\/arxiv.org\/abs\/1504.01842."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"1032","DOI":"10.1017\/S0960129512000850","article-title":"A certified lightweight non-interference Java bytecode verifier","volume":"23","author":"Barthe","year":"2013","journal-title":"Math. Struct. Comput. Sci."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Maiya, P., Kanade, A., and Majumdar, R. (2014, January 9\u201311). Race detection for Android applications. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201914, Edinburgh, UK.","DOI":"10.1145\/2594291.2594311"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1016\/bs.adcom.2017.12.006","article-title":"Chapter Seven - Event-Based Concurrency: Applications, Abstractions, and Analyses","volume":"112","author":"Kanade","year":"2019","journal-title":"Adv. Comput."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Ozkan, B.K., and Tasiran, S. (2017, January 22\u201329). Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. Proceedings of the Programming Languages and Systems 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, Uppsala, Sweden.","DOI":"10.1007\/978-3-662-54434-1_7"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Calzavara, S., Grishchenko, I., Koutsos, A., and Maffei, M. (2017). A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications. arXiv, Available online: https:\/\/arxiv.org\/pdf\/1705.10482.pdf.","DOI":"10.1109\/CSF.2017.19"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Calzavara, S., Grishchenko, I., and Maffei, M. (2016, January 21\u201324). HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving. Proceedings of the 2016 IEEE European Symposium on Security and Privacy (EuroSP), aarbrucken, Germany.","DOI":"10.1109\/EuroSP.2016.16"},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Chaudhuri, A. (2009, January 15\u201321). Language-based security on Android. Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, Dublin, Ireland.","DOI":"10.1145\/1554339.1554341"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Chen, T., He, J., Song, F., Wang, G., Wu, Z., and Yan, J. (2018, January 14\u201317). Android Stack Machine. Computer Aided Verification. Proceedings of the 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, Oxford, UK.","DOI":"10.1007\/978-3-319-96142-2_29"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"He, J., Chen, T., Wang, P., Wu, Z., and Yan, J. (2019, January 1\u20134). Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps. Proceedings of the Programming Languages and Systems - 17th Asian Symposium, Nusa Dua Bali, Indonesia.","DOI":"10.1007\/978-3-030-34175-6_15"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Bagheri, H., Kang, E., Malek, S., and Jackson, D. (2015, January 24\u201326). Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. Proceedings of the FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway.","DOI":"10.1007\/978-3-319-19249-9_6"},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Ren, L., Chang, R., Yin, Q., and Man, Y. (2017, January 12\u201315). A Formal Android Permission Model Based on the B Method. Proceedings of the Security, Privacy, and Anonymity in Computation, Communication, and Storage 10th International Conference, Guangzhou, China.","DOI":"10.1007\/978-3-319-72389-1_31"},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"16550","DOI":"10.1109\/ACCESS.2019.2895261","article-title":"Formal Analysis of Language-Based Android Security Using Theorem Proving Approach","volume":"7","author":"Khan","year":"2019","journal-title":"IEEE Access"},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"31358","DOI":"10.1109\/ACCESS.2019.2902608","article-title":"Acteve++: An Improved Android Application Automatic Tester Based on Acteve","volume":"7","author":"Qin","year":"2019","journal-title":"IEEE Access"},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Anand, S., Naik, M., Harrold, M.J., and Yang, H. (2012, January 11\u201316). Automated concolic testing of smartphone apps. Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), Cary, NC, USA.","DOI":"10.1145\/2393596.2393666"},{"key":"ref_36","unstructured":"Nisi, D., Bianchi, A., and Fratantonio, Y. (2019, January 23\u201325). Exploring Syscall-Based Semantics Reconstruction of Android Applications. Proceedings of the 22nd International Symposium on Research in Attacks, Intrusions and Defenses, Beijing, China."},{"key":"ref_37","unstructured":"Chin, E., Felt, A.P., Greenwood, K., and Wagner, D. (, January June). Analyzing Inter-application Communication in Android. Proceedings of the 9th International Conference on Mobile Systems, Applications, and Services, New York, NY, USA."},{"key":"ref_38","unstructured":"Drake, J.J., Lanier, Z., Mulliner, C., Fora, P.O., Ridley, S.A., and Wicherski, G. (2014). Android Hacker\u2019s Handbook, Wiley Publishing."},{"key":"ref_39","unstructured":"Android Open Source Project (AOSP) (2020, January 30). Dalvik Bytecode. Available online: https:\/\/source.android.com\/devices\/tech\/dalvik\/dalvik-bytecode."},{"key":"ref_40","unstructured":"Oracle Corporation (2019, October 02). Java Documentation on Thread. Available online: https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/lang\/Thread.html."},{"key":"ref_41","unstructured":"Oracle Corporation (2019, October 02). Java Documentation on Object. Available online: https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/lang\/Object.html."},{"key":"ref_42","unstructured":"G\u00f6ransson, A. (2014). Efficient Android Threading: Asynchronous Processing Techniques for Android Applications, O\u2019Reilly Media. [1st ed.]."},{"key":"ref_43","unstructured":"Davi, L., Dmitrienko, A., Sadeghi, A., and Winandy, M. (2010, January 25\u201328). Privilege Escalation Attacks on Android. Proceedings of the Information Security 13th International Conference, Boca Raton, FL, USA."}],"container-title":["Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2078-2489\/11\/3\/130\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T09:02:05Z","timestamp":1760173325000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2078-2489\/11\/3\/130"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,27]]},"references-count":43,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2020,3]]}},"alternative-id":["info11030130"],"URL":"https:\/\/doi.org\/10.3390\/info11030130","relation":{},"ISSN":["2078-2489"],"issn-type":[{"value":"2078-2489","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,27]]}}}