Ransomware Steals Your Phone. Formal Methods Rescue It

  • Francesco MercaldoEmail author
  • Vittoria Nardone
  • Antonella Santone
  • Corrado Aaron Visaggio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9688)


Ransomware is a recent type of malware which makes inaccessible the files or the device of the victim. The only way to unlock the infected device or to have the keys for decrypting the files is to pay a ransom to the attacker. Commercial solutions for removing ransomware and restoring the infected devices and files are ineffective, since this malware uses a very robust form of asymmetric cryptography and erases shadow copies and recovery points of the operating system. Literature does not count many solutions for effectively detecting and blocking ransomware and, at the best knowledge of the authors, formal methods were never applied to identify ransomware. In this paper we propose a methodology based on formal methods that is able to detect the ransomware and to identify in the malware’s code the instructions that implement the characteristic instructions of the ransomware. The results of the experimentation are strongly encouraging and suggest that the proposed methodology could be the right way to follow for developing commercial solutions that could successful intercept the ransomware and blocking the infections it provokes.


Malware Android Security Formal methods Temporal logic 


  1. 1.
    Anastasi, G., Bartoli, A., Francesco, N.D., Santone, A.: Efficient verification of a multicast protocol for mobile computing. Comput. J. 44(1), 21–30 (2001)CrossRefzbMATHGoogle Scholar
  2. 2.
    Andronio, N., Zanero, S., Maggi, F.: HelDroid: dissecting and detecting mobile ransomware. In: Bos, H., Monrose, F., Blanc, G. (eds.) RAID 2015. LNCS, vol. 9404, pp. 382–404. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-26362-5_18 CrossRefGoogle Scholar
  3. 3.
    Arp, D., Spreitzenbarth, M., Huebner, M., Gascon, H., Rieck, K.: Drebin: efficient and explainable detection of android malware in your pocket. In: Proceedings of 21st Annual Network and Distributed System Security Symposium (NDSS). IEEE (2014)Google Scholar
  4. 4.
    Barbuti, R., Francesco, N.D., Santone, A., Vaglini, G.: LORETO: a tool for reducing state explosion in verification of LOTOS programs. Softw. Pract. Exper. 29(12), 1123–1147 (1999)CrossRefGoogle Scholar
  5. 5.
    Battista, P., Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Identification of android malware families with model checking. In: International Conference on Information Systems Security and Privacy. SCITEPRESS (2016)Google Scholar
  6. 6.
    Canfora, G., Di Sorbo, A., Mercaldo, F., Visaggio, C.: Obfuscation techniques against signature-based detection: a case study. In: Proceedings of Workshop on Mobile System Technologies. IEEE (2015)Google Scholar
  7. 7.
    Ceccarelli, M., Cerulo, L., Ruvo, G.D., Nardone, V., Santone, A.: Infer gene regulatory networks from time series data with probabilistic model checking. In: 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE 2015, Florence, Italy, 18 May 2015, pp. 26–32. IEEE (2015)Google Scholar
  8. 8.
    Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  9. 9.
    De Francesco, N., Lettieri, G., Santone, A., Vaglini, G.: Heuristic search for equivalence checking. Softw. Syst. Model. 15(2), 513–530 (2016)CrossRefGoogle Scholar
  10. 10.
    Francesca, G., Santone, A., Vaglini, G., Villani, M.L.: Ant colony optimization for deadlock detection in concurrent systems. In: Proceedings of the 35th Annual IEEE International Computer Software and Applications Conference, COMPSAC 2011, Munich, Germany, 18–22 July 2011, pp. 108–117. IEEE (2011)Google Scholar
  11. 11.
    Francesco, N.D., Santone, A., Vaglini, G.: State space reduction by non-standard semantics for deadlock analysis. Sci. Comput. Program. 30(3), 309–338 (1998)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Jacob, G., Filiol, E., Debar, H.: Formalization of viruses and malware through process algebras. In: International Conference on Availability, Reliability and Security (ARES 2010). IEEE (2010)Google Scholar
  13. 13.
    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
  14. 14.
    Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Download malware? No, thanks. How formal methods can block update attacks. In: 2016 IEEE/ACM 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE). IEEE (2016)Google Scholar
  15. 15.
    Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  16. 16.
    Song, F., Touili, T.: Pommade: pushdown model-checking for malware detection. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM (2013)Google Scholar
  17. 17.
    Song, F., Touili, T.: Model-checking for android malware detection. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 216–235. Springer, Heidelberg (2014)Google Scholar
  18. 18.
    Spreitzenbarth, M., Echtler, F., Schreck, T., Freling, F.C., Hoffmann, J.: Mobilesandbox: looking deeper into android applications. In: 28th International ACM Symposium on Applied Computing (SAC). ACM (2013)Google Scholar
  19. 19.
    Stirling, C.: An introduction to modal and temporal logics for CCS. In: Ito, T. (ed.) UK/Japan WS 1989. LNCS, vol. 491, pp. 1–20. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  20. 20.
    Yang, T., Yang, Y., Qian, K., Lo, D.C.T., Qian, Y., Tao, L.: Automated detection and analysis for android ransomware. In: HPCC/CSS/ICESS, pp. 1338–1343. IEEE (2015)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2016

Authors and Affiliations

  • Francesco Mercaldo
    • 1
    Email author
  • Vittoria Nardone
    • 1
  • Antonella Santone
    • 1
  • Corrado Aaron Visaggio
    • 1
  1. 1.Department of EngineeringUniversity of SannioBeneventoItaly

Personalised recommendations