{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:17:03Z","timestamp":1725981423966},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319941103"},{"type":"electronic","value":"9783319941110"}],"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-94111-0_1","type":"book-chapter","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:07:44Z","timestamp":1529075264000},"page":"3-25","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Software Model Checking for Mobile Security \u2013 Collusion Detection in $$\\mathbb {K}$$K"],"prefix":"10.1007","author":[{"given":"Irina M\u0103riuca","family":"As\u0103voae","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hoang Nga","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Roggenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,16]]},"reference":[{"key":"1_CR1","unstructured":"Android API reference. \nhttps:\/\/developer.android.com\/reference\/classes\n\n. Accessed 01 May 2018"},{"key":"1_CR2","unstructured":"Android bytecode. \nhttps:\/\/source.android.com\/devices\/tech\/dalvik\/dalvik-bytecode\n\n. Accessed 01 May 2018"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Alam, M.I., Halder, R., Goswami, H., Pinto, J.S.: K-taint: an executable rewriting logic semantics for taint analysis in the k-framework. In: ENASE, pp. 359\u2013366. SciTePress (2018)","DOI":"10.5220\/0006786603590366"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Arzt, S., Rasthofer, S., Fritz, C., Bodden, E., Bartel, A., Klein, J., Traon, Y.L., Octeau, D., McDaniel, P.: FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In: PLDI 2014, p. 29. ACM (2014)","DOI":"10.1145\/2666356.2594299"},{"key":"1_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59439-2_3","volume-title":"Data Analytics and Decision Support for Cybersecurity","author":"IM Asavoae","year":"2017","unstructured":"Asavoae, 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 Android$$^{TM}$$TM case. In: Carrascosa, I.P., Kalutarage, H.K., Huang, Y. (eds.) Data Analytics and Decision Support for Cybersecurity. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-59439-2_3"},{"key":"1_CR6","unstructured":"Asavoae, I.M., Blasco, J., Chen, T.M., Kalutarage, H.K., Muttik, I., Nguyen, H.N., Roggenbach, M., Shaikh, S.A.: Distinguishing between malicious app collusion and benign app collaboration: a machine learning approach. Virus Bulletin (2018)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Asavoae, I.M., Nguyen, H.N., Roggenbach, M., Shaikh, S.A.: Utilising $$\\mathbb{K}$$K semantics for collusion detection in Android applications. In: ter Beek, M.H., Gnesi, S., Knapp, A. (eds.) FMICS-AVoCS 2016, pp. 142\u2013149 (2016)","DOI":"10.1007\/978-3-319-45943-1_10"},{"key":"1_CR8","unstructured":"Asavoae, I.M., Nguyen, H.N., Roggenbach, M., Shaikh, S.A.: Software model checking: a promising approach to verify mobile app security. CoRR abs\/1706.04741 (2017). \nhttp:\/\/arxiv.org\/abs\/1706.04741"},{"key":"1_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_16","volume-title":"Handbook on Model Checking","author":"D Beyer","year":"2018","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.: Combining model checking and data-flow analysis. In: Clarke, E.M., Henzinger, T.A., Veith, H. (eds.) Handbook on Model Checking. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10575-8_16"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.jnca.2017.12.008","volume":"105","author":"J Blasco","year":"2018","unstructured":"Blasco, J., Chen, T.M., Muttik, I., Roggenbach, M.: Detection of app collusion potential using logic programming. J. Netw. Comput. Appl. 105, 88\u2013104 (2018). \nhttps:\/\/doi.org\/10.1016\/j.jnca.2017.12.008","journal-title":"J. Netw. Comput. Appl."},{"key":"1_CR12","unstructured":"Blasco, J., Muttik, I., Roggenbach, M.: Wild android collusions (2016). \nhttps:\/\/www.virusbulletin.com\/conference\/vb2016\/"},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1145\/2775051.2676982","volume":"50","author":"Denis Bogdanas","year":"2015","unstructured":"Bogd\u0103na\u015f, D., Ro\u015fu, G.: K-Java: a complete semantics of Java. In: POPL 2015. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Bugiel, S., Davi, L., Dmitrienko, A., Heuser, S., Sadeghi, A.R., Shastry, B.: Practical and lightweight domain isolation on Android. In: SPSM 2011. ACM (2011)","DOI":"10.1145\/2046614.2046624"},{"key":"1_CR15","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: How to Specify, Program and Verify Systems in Rewriting Logic","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"1_CR16","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16310-4_8"},{"key":"1_CR17","unstructured":"Dicker, C.: Android security: delusion to collusion. B.Sc. dissertation, Swansea University (2015)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Hathhorn, C., Ellison, C., Ro\u015fu, G.: Defining the undefinedness of C. In: PLDI 2015. ACM (2015)","DOI":"10.1145\/2737924.2737979"},{"issue":"3","key":"1_CR19","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/s11235-017-0296-1","volume":"66","author":"HK Kalutarage","year":"2017","unstructured":"Kalutarage, H.K., Nguyen, H.N., Shaikh, S.A.: Towards a threat assessment framework for apps collusion. Telecommun. Syst. 66(3), 417\u2013430 (2017). \nhttps:\/\/doi.org\/10.1007\/s11235-017-0296-1","journal-title":"Telecommun. Syst."},{"key":"1_CR20","unstructured":"Kovacs, E.: Malware abuses Android accessibility feature to steal data (2015). \nhttp:\/\/www.securityweek.com\/malware-abuses-android-accessibility-feature-steal-data"},{"issue":"7","key":"1_CR21","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"1_CR22","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-319-18467-8_34","volume-title":"ICT Systems Security and Privacy Protection","author":"L Li","year":"2015","unstructured":"Li, L., Bartel, A., Bissyand\u00e9, T.F., Klein, J., Le Traon, Y.: ApkCombiner: combining multiple android apps to support inter-app analysis. In: Federrath, H., Gollmann, D. (eds.) SEC 2015. IAICT, vol. 455, pp. 513\u2013527. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-18467-8_34"},{"key":"1_CR23","unstructured":"Lipovsky, R.: ESET analyzes first Android file-encrypting, TOR-enabled ransomware (2014). \nhttp:\/\/www.welivesecurity.com\/2014\/06\/04\/simplocker\/"},{"key":"1_CR24","unstructured":"Lunden, I.: 6.1B Smartphone Users Globally By 2020, Overtaking Basic Fixed Phone Subscriptions. \nhttp:\/\/techcrunch.com\/2015\/06\/02\/6-1b-smartphone-users-globally-by-2020-overtaking-basic-fixed-phone-subscriptions\/#.pkatr9:RPIH\n\n. Accessed 10 Nov 2015"},{"key":"1_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/978-3-662-03811-6"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Octeau, D., Luchaup, D., Dering, M., Jha, S., McDaniel, P.: Composite constant propagation: application to Android inter-component communication analysis. In: ICSE 2015. IEEE Computer Society (2015)","DOI":"10.1109\/ICSE.2015.30"},{"issue":"11","key":"1_CR27","doi-asserted-by":"publisher","first-page":"999","DOI":"10.1109\/TSE.2016.2550446","volume":"42","author":"D Octeau","year":"2016","unstructured":"Octeau, D., Luchaup, D., Jha, S., McDaniel, P.D.: Composite constant propagation and its application to Android program analysis. IEEE Trans. Softw. Eng. 42(11), 999\u20131014 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR28","unstructured":"Octeau, D., McDaniel, P., Jha, S., Bartel, A., Bodden, E., Klein, J., Traon, Y.L.: Effective inter-component communication mapping in Android: an essential step towards holistic security analysis. In: Security Symposium. USENIX Association (2013)"},{"key":"1_CR29","unstructured":"Page, C.: MKero: Android malware secretly subscribes victims to premium SMS services (2015). \nhttp:\/\/www.theinquirer.net\/inquirer\/news\/2425201\/mkero-android-malware-secretly-subscribes-victims-to-premium-sms-services"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Ravitch, T., Creswick, E.R., Tomb, A., Foltzer, A., Elliott, T., Casburn, L.: Multi-app security analysis with FUSE: statically detecting Android app collusion. In: ACSAC 2014. ACM (2014)","DOI":"10.1145\/2689702.2689705"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1007\/978-3-319-23165-5_28","volume-title":"Logic, Rewriting, and Concurrency","author":"G Ro\u015fu","year":"2015","unstructured":"Ro\u015fu, G.: From rewriting logic, to programming language semantics, to program verification. In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 598\u2013616. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23165-5_28"},{"key":"1_CR32","unstructured":"Ro\u015fu, G.: Matching logic. In: RTA 2015. LIPIcs, vol. 36, pp. 5\u201321. SchlossDagstuhl\u2013Leibniz-Zentrum fuer Informatik, July 2015"},{"issue":"6","key":"1_CR33","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Logic Algebraic Program."},{"key":"1_CR34","unstructured":"Schlegel, R., Zhang, K., Zhou, X.y., Intwala, M., Kapadia, A., Wang, X.: Soundcomber: a stealthy and context-aware sound Trojan for smartphones. In: NDSS, vol. 11, pp. 17\u201333 (2011)"},{"issue":"2","key":"1_CR35","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1109\/SURV.2013.101613.00077","volume":"16","author":"G Suarez-Tangil","year":"2014","unstructured":"Suarez-Tangil, G., Tapiador, J.E., Peris-Lopez, P., Ribagorda, A.: Evolution, detection and analysis of malware for smart devices. IEEE Commun. Surv. Tutor. 16(2), 961\u2013987 (2014)","journal-title":"IEEE Commun. Surv. Tutor."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94111-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:08:01Z","timestamp":1529075281000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94111-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319941103","9783319941110"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94111-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}