Android malware has been increasingly identified and organised into families [28, 36], e.g., Geinimi, Basebridge, Spitmo, Zitmo, and Ginmaster, etc. This human-decided organisation was based on some unexpected behaviours exhibited in malware instances, e.g., intercept incoming messages then send them out via Internet connections, load classes from a hidden payload then execute commands from remote servers, and send premium messages constantly, and so on;and malware instances in one family share some common unexpected behaviours [17, 29]. We study the problem of verifying Android applications to deny these behaviours. That is, (a) to formalise and learn unexpected behaviours from malware instances exploiting their family information, so-called anti-security policies; (b) and verify target applications against these policies efficiently, so as to decide whether a target application has any unexpected behaviour. Our main contributions are : (a) we implement a static analysis tool to construct an extended B¨ uchi automaton for each Android application to approximate its behaviours, considering a broad range of features of Java and the Android framework ;(b) we develop an efficient machine-learning-centred method to construct sub-automata as anti-security policies from thousands of malware instances across hundreds of malware families; (c) we demonstrate the effectiveness of antisecurity policy verification by showing how it helps reveal covert channels in a scenario of collusion attacks. We show that using the verification results against anti-security policies as input features, the classification performance on new malware detections is improved dramatically, in particular, the precision and recall are respectively 8% and 51% better than those using APIs calls and permissions as input features. We compare anti-security policies for malware families to their manual descriptions, which have been produced by malware analysts or third-party researchers [1, 2, 4, 5, 23],and demonstrate they compare well to these descriptions. This research has several potential benefits, including: help people get better understanding of potential threats hidden in mobile applications; provide hints for malware analysts before more expensive investigation; support automatic generation of malware analysis reports; and provide clear and friendly references for security policy designers, etc.
|Title of host publication||Fourth International Seminar on Program Verification, Automated Debugging and Symbolic Computation|
|Number of pages||6|
|Publication status||Published - 21 Oct 2015|