Model-Checking for Android Malware Detection
作者： Fu Song , Tayssir Touili
DOI: 10.1007/978-3-319-12736-1_12
关键词:
摘要: The popularity of Android devices results in a significant increase malwares. These malwares commonly steal users’ private data or do malicious tasks. Therefore, it is important to efficiently and automatically analyze applications identify their behaviors. This paper introduces an automatic scalable approach applications. Our consists modeling application as PushDown System (PDS), succinctly specifying behaviors Computation Tree Logic (CTL) Linear Temporal (LTL), reducing the malware detection problem CTL/LTL model-checking for PDSs. We implemented our techniques tool applied more than 1260 android obtained encouraging results. In particular, we discovered ten programs known benign that are leaking data.
springer.com
sci-hub.st 参考文章(32)
Fu Song, Tayssir Touili, Efficient Malware Detection Using Model-Checking formal methods. pp. 418- 433 ,(2012) , 10.1007/978-3-642-32759-9_34
Damien Octeau, William Enck, Patrick McDaniel, Swarat Chaudhuri, A study of android application security usenix security symposium. pp. 21- 21 ,(2011)
Clint Gibler, Jonathan Crussell, Jeremy Erickson, Hao Chen, AndroidLeaks: automatically detecting potential privacy leaks in android applications on a large scale trust and trustworthy computing. pp. 291- 307 ,(2012) , 10.1007/978-3-642-30921-2_17
Fu Song, Tayssir Touili, LTL model-checking for malware detection tools and algorithms for construction and analysis of systems. pp. 416- 431 ,(2013) , 10.1007/978-3-642-36742-7_29
Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon, Efficient Algorithms for Model Checking Pushdown Systems computer aided verification. pp. 232- 247 ,(2000) , 10.1007/10722167_20
Akash Lal, Thomas Reps, Gogul Balakrishnan, Extended Weighted Pushdown Systems Computer Aided Verification. pp. 434- 448 ,(2005) , 10.1007/11513988_44
Mihai Christodorescu, Somesh Jha, Static analysis of executables to detect malicious patterns usenix security symposium. pp. 12- 12 ,(2003) , 10.21236/ADA449067
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Ahmed Bouajjani, Javier Esparza, Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking international conference on concurrency theory. pp. 135- 150 ,(1997) , 10.1007/3-540-63141-0_10
Shashi Shekhar, Michael Dietz, Anhei Shu, Dan S. Wallach, Yuliy Pisetsky, Quire: lightweight provenance for smart phone operating systems usenix security symposium. pp. 23- 23 ,(2011)