Model-Checking for Android Malware Detection

  • Fu Song
  • Tayssir Touili
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)


The popularity of Android devices results in a significant increase of Android malwares. These malwares commonly steal users’ private data or do malicious tasks. Therefore, it is important to efficiently and automatically analyze Android applications and identify their malicious behaviors. This paper introduces an automatic and scalable approach to analyze Android applications and identify malicious applications. Our approach consists of modeling an Android application as a PushDown System (PDS), succinctly specifying malicious behaviors in Computation Tree Logic (CTL) or Linear Temporal Logic (LTL), and reducing the Android malware detection problem to CTL/LTL model-checking for PDSs. We implemented our techniques in a tool and applied it to analyze more than 1260 android applications. We obtained encouraging results. In particular, we discovered ten programs known as benign that are leaking private data.


Control Point Transition Rule Private Data Linear Temporal Logic Malicious Behavior 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)Google Scholar
  2. 2.
    Beresford, A.R., Rice, A., Skehin, N., Sohan, R.: Mockdroid: Trading privacy for application functionality on smartphones. In: HotMobile, pp. 49–54 (2011)Google Scholar
  3. 3.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)Google Scholar
  4. 4.
    Bugiel, S., Davi, L., Dmitrienko, A., Fischer, T., Sadeghi, A.-R., Shastry, B.: Towards taming privilege-escalation attacks on android. In: NDSS (2012)Google Scholar
  5. 5.
    Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. In: 12th USENIX Security Symposium, pp. 169–186 (2003)Google Scholar
  6. 6.
    Christodorescu, M., Jha, S., Seshia, S.A., Song, D.X., Bryant, R.E.: Semantics-aware malware detection. In: IEEE Symposium on Security and Privacy, pp. 32–46 (2005)Google Scholar
  7. 7.
    Dietz, M., Shekhar, S., Pisetsky, Y., Shu, A., Wallach, D.S.: Quire: Lightweight provenance for smart phone operating systems. In: USENIX Security Symposium (2011)Google Scholar
  8. 8.
    Enck, W., Gilbert, P., Gon Chun, B., Cox, L.P., Jung, J., McDaniel, P., Sheth, A.: Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones. In: OSDI (2010)Google Scholar
  9. 9.
    Enck, W., Octeau, D., McDaniel, P., Chaudhuri, S.: A study of android application security. In: USENIX Security Symposium (2011)Google Scholar
  10. 10.
    Enck, W., Ongtang, M., McDaniel, P.D.: On lightweight mobile phone application certification. In: ACM Conference on Computer and Communications Security (2009)Google Scholar
  11. 11.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithm for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 232–247. Springer, Heidelberg (2000)Google Scholar
  12. 12.
    Felt, A.P., Wang, H.J., Moshchuk, A., Hanna, S., Chin, E.: Permission re-delegation: Attacks and defenses. In: USENIX Security Symposium (2011)Google Scholar
  13. 13.
    Gibler, C., Crussell, J., Erickson, J., Chen, H.: AndroidLeaks: Automatically detecting potential privacy leaks in android applications on a large scale. In: Katzenbeisser, S., Weippl, E., Camp, L.J., Volkamer, M., Reiter, M., Zhang, X. (eds.) TRUST 2012. LNCS, vol. 7344, pp. 291–307. Springer, Heidelberg (2012)Google Scholar
  14. 14.
    Grace, M.C., Zhou, Y., Zhang, Q., Zou, S., Jiang, X.: Riskranker: Scalable and accurate zero-day android malware detection. In: MobiSys (2012)Google Scholar
  15. 15.
    Hornyack, P., Han, S., Jung, J., Schechter, S.E., Wetherall, D.: These aren’t the droids you’re looking for: retrofitting android to protect data from imperious applications. In: ACM CCS, pp. 639–652 (2011)Google Scholar
  16. 16.
    Kim, J., Yoon, Y., Yi, K., Shin, J.: Scandal: Static analyzer for detecting privacy leaks in android application. In: Mobile Security Technologies 2012 (2012)Google Scholar
  17. 17.
    Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Detecting malicious code by model checking. In: Julisch, K., Kruegel, C. (eds.) DIMVA 2005. LNCS, vol. 3548, pp. 174–187. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  18. 18.
    Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 434–448. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Mann, C., Starostin, A.: A framework for static detection of privacy leaks in android applications. In: SAC, pp. 1457–1462 (2012)Google Scholar
  20. 20.
    Nauman, M., Khan, S., Zhang, X.: Apex: Extending android permission model and enforcement with user-defined runtime constraints. In: ASIACCS, pp. 328–332 (2010)Google Scholar
  21. 21.
    Octeau, D., Jha, S., McDaniel, P.: Retargeting Android applications to Java bytecode. In: SIGSOFT FSE (2012)Google Scholar
  22. 22.
    Ongtang, M., McLaughlin, S.E., Enck, W., McDaniel, P.D.: Semantically rich application-centric security in android. In: ACSAC (2009)Google Scholar
  23. 23.
    Reps, T.W., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 189–213. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  24. 24.
    Singh, P.K., Lakhotia, A.: Static verification of worm and virus behavior in binary executables using model checking. In: IAW, pp. 298–300 (2003)Google Scholar
  25. 25.
    Song, F., Touili, T.: Efficient malware detection using model-checking. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 418–433. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  26. 26.
    Song, F., Touili, T.: Pushdown model checking for malware detection. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 110–125. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  27. 27.
    Song, F., Touili, T.: LTL model-checking for malware detection. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 416–431. Springer, Heidelberg (2013)Google Scholar
  28. 28.
    Song, F., Touili, T.: Model-checking for Android Malware Detection. Technical report, Shanghai Key Laboratory of Trustworthy Computing (2014),
  29. 29.
    Zhou, Y., Jiang, X.: Dissecting android malware: Characterization and evolution. In: IEEE Symposium on Security and Privacy, pp. 95–109 (2012)Google Scholar
  30. 30.
    Zhou, Y., Wang, Z., Zhou, W., Jiang, X.: Hey, you, get off of my market: Detecting malicious apps in official and alternative android markets. In: NDSS (2012)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Fu Song
    • 1
  • Tayssir Touili
    • 2
  1. 1.Shanghai Key Laboratory of Trustworthy ComputingEast China Normal UniversityP.R. China
  2. 2.CNRS and Université Paris DiderotFrance

Personalised recommendations