Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
International Journal of Information Security
Published in: International Journal of Information Security 6/2018

19-12-2017 | Regular Contribution

Talos: no more ransomware victims with formal methods

Authors: Aniello Cimitile, Francesco Mercaldo, Vittoria Nardone, Antonella Santone, Corrado Aaron Visaggio

Published in: International Journal of Information Security | Issue 6/2018

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Ransomware is a very effective form of malware that is recently spreading out on an impressive number of workstations and smartphones. This malware blocks the access to the infected machine or to the files located in the infected machine. The attackers will restore the machine and files only after the payment of a certain amount of money, usually given in the form of bitcoins. Commercial solutions are still ineffective to recognize the last variants of ransomware, and the problem has been poorly investigated in literature. In this paper we discuss a methodology based on formal methods for detecting ransomware malware on Android devices. We have implemented our method in a tool named Talos. We evaluate the method, and the obtained results show that Talos is very effective in recognizing ransomware (accuracy of 0.99) even when it is obfuscated (accuracy still remains at 0.99).
previous article Comparing apples with apples: performance analysis of lattice-based authenticated key exchange protocols

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
Footnotes
Literature
1.
Anderson, B., Quist, D., Neil, J., Storlie, C., Lane, T.: Graph-based malware detection using dynamic analysis. J. Comput. Virol. 7(4), 247–258 (2011)CrossRef
2.
Andronio, N., Zanero, S., Maggi, F.: Heldroid: Dissecting and detecting mobile ransomware. In: International Workshop on Recent Advances in Intrusion Detection, pp. 382–404. Springer (2015)
3.
Annachhatre, C., Austin, T.H., Stamp, M.: Hidden markov models for malware classification. J. Comput. Virol. Hacking Tech. 11(2), 59–73 (2015)CrossRef
4.
Arp, D., Spreitzenbarth, M., Huebner, M., Gascon, H., Rieck, K.: Drebin: efficient and explainable detection of android malware in your pocket. In: Proceedings of 21th Annual Network and Distributed System Security Symposium (NDSS), IEEE (2014)
5.
Attaluri, S., McGhee, S., Stamp, M.: Profile hidden markov models and metamorphic virus detection. J. Comput. Virol. 5(2), 151–169 (2009)CrossRef
6.
Aurangzeb, S., Aleem, M., Iqbal, M.A., Islam, M.A.: Ransomware: a survey and trends. J. Inf. Assur. Secur. 6(2), 48–58 (2017)
7.
Battista, P., Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.: Identification of android malware families with model checking. In: International Conference on Information Systems Security and Privacy, SCITEPRESS (2016)
8.
Bayer, U., Moser, A., Kruegel, C., Kirda, E.: Dynamic analysis of malicious code. J. Comput. Virol. 2(1), 67–77 (2006)CrossRef
9.
Burguera, I., Zurutuza, U., Nadjm-Tehrani, S.: Crowdroid: behavior-based malware detection system for android. In: Proceedings of the 1st ACM Workshop on Security and Privacy in Smartphones and Mobile Devices, ACM, pp. 15–26 (2011)
10.
Canfora, G., De Lorenzo, A., Medvet, E., Mercaldo, F., Visaggio, C.A.: Effectiveness of opcode ngrams for detection of multi family android malware. In: 2015 10th International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 333–340 (2015)
11.
Canfora, G., Di Sorbo, A., Mercaldo, F., Visaggio, C. A.: Obfuscation techniques against signature-based detection: a case study. In: 2015 Mobile Systems Technologies Workshop (MST), IEEE, pp. 21–26 (2015)
12.
Canfora, G., Medvet, E., Mercaldo, F., Visaggio, C.A.: Detecting android malware using sequences of system calls. In: Proceedings of the 3rd International Workshop on Software Development Lifecycle for Mobile, ACM, pp. 13–20 (2015)
13.
Canfora, G., Mercaldo, F., Moriano, G., Visaggio, C.A.: Composition-malware: building android malware at run time. In: 2015 10th International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 318–326 (2015)
14.
Canfora, G., Mercaldo, F., Visaggio, C.A.: A classifier of malicious android applications. In: 2013 Eighth International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 607–614 (2013)
15.
Canfora, G., Mercaldo, F., Visaggio, C.A.: Evaluating op-code frequency histograms in malware and third-party mobile applications. In: E-Business and Telecommunications, Springer, pp. 201–222 (2015)
16.
Canfora, G., Mercaldo, F., Visaggio, C.A.: Mobile malware detection using op-code frequency histograms. In: Proceedings of International Conference on Security and Cryptography (SECRYPT) (2015)
17.
Canfora, G., Mercaldo, F., Visaggio, C.A.: An hmm and structural entropy based detector for android malware: an empirical study. Comput. Secur. 61, 1–18 (2016)CrossRef
18.
Carter, H., Mood, B., Traynor, P., Butler, K.R.B.: Secure outsourced garbled circuit evaluation for mobile devices. J. Comput. Secur. 24(2), 137–180 (2015)CrossRef
19.
Chenette, S.: The ultimate deobfuscator. In: Proceedings of the ToorConX Conference (2008)
20.
Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. Technical Report, DTIC Document (2006)
21.
Christodorescu, M., Jha, S., Seshia, S.A., Song, D., Bryant, R.E.: Semantics-aware malware detection. In: 2005 IEEE Symposium on Security and Privacy (S&P’05), IEEE, pp. 32–46 (2005)
22.
Cimitile, A., Mercaldo, F., Martinelli, F., Nardone, V., Santone, A., Vaglini, G.: Model checking for mobile android malware evolution. In: Proceedings of the 5th International FME Workshop on Formal Methods in Software Engineering, FormaliSE ’17, Piscataway, NJ, USA, IEEE Press, pp. 24–30 (2017)
23.
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)CrossRef
24.
Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV. Lecture Notes in Computer Science, vol. 1102. Springer, Berlin (1996)
25.
di Vimercati, S.D.C., Foresti, S., Livraga, G., Samarati, P.: Data privacy: definitions and techniques. Int. J. Uncertain. Fuzziness Knowl. Based Syst. 20(6), 793–818 (2012)CrossRef
26.
27.
Faruki, P., Bharmal, A., Laxmi, V., Ganmoor, V., Gaur, M.S., Conti, M., Rajarajan, M.: Android security: a survey of issues, malware penetration, and defenses. Commun. Surv. Tutor. IEEE 17(2), 998–1022 (2015)CrossRef
28.
Feinstein, B., Peck, D., SecureWorks, I.: Caffeine monkey: automated collection, detection and analysis of malicious javascript. In: Black Hat, USA (2007)
29.
30.
Ford, S., Cova, M., Kruegel, C., Vigna, G.: Analyzing and detecting malicious flash advertisements. In: Proceedings of the Computer Security Applications Conference, 2009. ACSAC’09. Annual. pp. 363–372. IEEE (2009)
31.
Francesco, N.D., Santone, A., Vaglini, G.: A user-friendly interface to specify temporal properties of concurrent systems. Inf. Sci. 177(1), 299–311 (2007)CrossRef
32.
Gharacheh, M., Derhami, V., Hashemi, S., Fard, S.M.H.: Detection of metamorphic malware based on hmm: a hierarchical approach. Int. J. Intell. Syst. Appl. 8(4), 18 (2016)
33.
Hallaraker, O., Vigna, G.: Detecting malicious javascript code in mozilla. In: 10th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS’05), IEEE, pp. 85–94 (2005)
34.
Hampton, N., Baig, Z.A.: Ransomware: emergence of the cyber-extortion menace In: Proceedings of the 13th Australian Information Security Management Conference, 2015. pp. 47–56. SRI Security Research Institute, Edith Cowan University (2015)
35.
Hartstein, B.: Jsunpack: an automatic javascript unpacker. In: ShmooCon Convention (2009)
36.
Jackson, W.: An introduction to the android application development platform. In: Android Apps for Absolute Beginners, Springer, pp. 61–99 (2014)
37.
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)
38.
Jang, J., Woo, M., Brumley, D.: Towards automatic software lineage inference. In: USENIX Security, pp. 81–96 (2013)
39.
40.
Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Detecting Malicious Code by Model Checking. Springer, Berlin (2005)CrossRef
41.
Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)CrossRef
42.
Li, J., Xu, M., Zheng, N., Xu, J.: Malware obfuscation detection via maximal patterns. In: Third International Symposium on Intelligent Information Technology Application, IITA 2009, vol 2, IEEE, pp. 324–328 (2009)
43.
Likarish, P., Jung, E., Jo, I.: Obfuscated malicious javascript detection using classification techniques. In: MALWARE, Citeseer, pp. 47–54 (2009)
44.
Liu, X., Liu, J.: A two-layered permission-based android malware detection scheme. In: 2014 2nd IEEE International Conference on Mobile Cloud Computing, Services, and Engineering (MobileCloud), IEEE, pp. 142–148 (2014)
45.
Maier, D., Müller, T., Protsenko, M.: Divide-and-conquer: why android malware cannot be stopped. In: 2014 Ninth International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 30–39 (2014)
46.
Mercaldo, F., Nardone, V., Santone, A.: Ransomware inside out. In: 2016 11th International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 628–637 (2016)
47.
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)
48.
Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Hey malware, I can find you! In: 25th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE Workshops 2016, Paris, June 13–15 (2016)
49.
Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Ransomware steals your phone formal methods rescue it. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Springer, pp. 212–221 (2016)
50.
Mercaldo, F., Visaggio, C.A., Canfora, G., Cimitile, A.: Mobile malware detection in the real world. In: Proceedings of the 38th International Conference on Software Engineering Companion, ACM, pp. 744–746 (2016)
51.
52.
Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)MATH
53.
Moser, A., Kruegel, C., Kirda, E.: Limits of static analysis for malware detection. In: Twenty-Third Annual Computer Security Applications Conference, ACSAC 2007, IEEE, pp. 421–430 (2007)
54.
Muttoo, S.K., Badhani, S.: Android malware detection: state of the art. Int. J. Inf. Technol. 9(1), 111–117 (2017)
55.
Oh, H.-S., Yeo, J.H., Moon, S.-M.: Bytecode-to-c ahead-of-time compilation for android Dalvik virtual machine. In: Proceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, EDA Consortium, pp. 1048–1053 (2015)
56.
Preda, M.D., Christodorescu, M., Jha, S., Debray, S.: A semantics-based approach to malware detection. ACM Trans. Progr. Lang. Syst. (TOPLAS) 30(5), 25 (2008)MATH
57.
Preda, M.D., Giacobazzi, R.: Semantics-based code obfuscation by abstract interpretation. J. Comput. Secur. 17(6), 855–908 (2009)CrossRef
58.
Rastogi, V., Chen, Y., Jiang, X.: Droidchameleon: evaluating android anti-malware against transformation attacks. In: Proceedings of the 8th ACM SIGSAC Symposium on Information, Computer and Communications Security, ACM, pp. 329–334 (2013)
59.
Rastogi, V., Chen, Y., Jiang, X.: Catch me if you can: evaluating android anti-malware against transformation attacks. IEEE Trans. Inf. Forensics Secur. 9(1), 99–108 (2014)CrossRef
60.
Ren, K., Samarati, P., Gruteser, M., Ning, P., Liu, Y.: Guest editorial special issue on security for iot: the state of the art. IEEE Internet Things J. 1(5), 369–371 (2014)CrossRef
61.
Rieck, K., Holz, T., Willems, C., Düssel, P., Laskov, P.: Learning and classification of malware behavior. In: International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment, Springer, pp. 108–125 (2008)
62.
Rieck, K., Trinius, P., Willems, C., Holz, T.: Automatic analysis of malware behavior using machine learning. J. Comput. Secur. 19(4), 639–668 (2011)CrossRef
63.
64.
65.
Song, F., Touili, T.: Efficient Malware Detection Using Model-Checking. Springer, Berlin (2001)MATH
66.
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)
67.
Song, F., Touili, T.: Model-Checking for Android Malware Detection. Springer, Berlin (2014)CrossRef
68.
Song, J., Han, C., Wang, K., Zhao, J., Ranjan, R., Wang, L.: An integrated static detection and analysis framework for android. Pervasive Mob. Comput. 32, 1–11 (2016)CrossRef
69.
Song, S., Kim, B., Lee, S.: The effective ransomware prevention technique using process monitoring on android platform. Mob. Inf. Syst. 2016, 1–9 (2016)
70.
71.
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)
72.
Stirling, C.: An introduction to modal and temporal logics for CCS. In: Yonezawa, A., Ito, T. (eds.) Concurrency: Theory, Language, And Architecture (LNCS), pp. 2–20. Springer, Berlin (1989)
73.
Sung, A.H., Xu, J., Chavez, P., Mukkamala, S.: Static analyzer of vicious executables (save). In: 20th Annual Computer Security Applications Conference, IEEE, pp. 326–334 (2004)
74.
Tan, D.J., Chua, T.-W., Thing, V.L., et al.: Securing android: a survey, taxonomy, and challenges. ACM Comput. Surv. (CSUR) 47(4), 58 (2015)
75.
Willems, C., Holz, T., Freiling, F.: Toward automated dynamic malware analysis using cwsandbox. IEEE Secur. Priv. 5(2), 32–39 (2007)CrossRef
76.
Yang, T., Yang, Y., Qian, K., Lo, D.C.-T., Qian, Y., Tao, L.: Automated detection and analysis for android ransomware. In: 7th International Symposium on Cyberspace Safety and Security (CSS), IEEE, pp. 1338–1343 (2015)
77.
Zheng, M., Lee, P.P., Lui, J.C.: Adam: an automatic and extensible platform to stress test android anti-virus systems. In: International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment, Springer, pp. 82–101 (2012)
Metadata
Title
Talos: no more ransomware victims with formal methods
Authors
Aniello Cimitile
Francesco Mercaldo
Vittoria Nardone
Antonella Santone
Corrado Aaron Visaggio
Publication date
19-12-2017
Publisher
Springer Berlin Heidelberg
Published in
International Journal of Information Security / Issue 6/2018
Print ISSN: 1615-5262
Electronic ISSN: 1615-5270
DOI
https://doi.org/10.1007/s10207-017-0398-5

Other articles of this Issue 6/2018

International Journal of Information Security 6/2018 Go to the issue

Regular Contribution

Optimal noise functions for location privacy on continuous regions

Regular Contribution

Optimization algorithm for k-anonymization of datasets with low information loss

Regular Contribution

DomainProfiler: toward accurate and early discovery of domain names abused in future

Regular Contribution

OnionDNS: a seizure-resistant top-level domain

Regular Contribution

A framework for estimating information security risk assessment method completeness

Regular Contribution

Comparing apples with apples: performance analysis of lattice-based authenticated key exchange protocols

Premium Partner

    Image Credits