Talos: no more ransomware victims with formal methods

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).