Formal Methods for Android Banking Malware Analysis and Detection

The Android operating system has been dominating the smart devices market in recent years. Smart home devices are populating our houses and smartphones are indispensable companions in daily life activities. In such a technological environment, the amount of data and user information shared across these devices is enormous and attractive for every malicious user. Consequently, developing good malware detection techniques is a crucial open problem to keep using these devices safely. This paper proposes the application of a formal methods based approach to detect banking malware in the Android environment. The experimental results are really promising, as demonstrated by the evaluation on real-world Android applications, where we reached precision and recall equal to 1.