Twinkle Twinkle Little DroidDream, How I Wonder What You Are?

Android is the most diffused environment for embedded systems. Not only mobile devices are Android powered, as matter of fact also in automotive and robotics fields, customized Android versions are currently employed. While Android offers several pro, from the stable kernel to the no usage of royalties, there are also cons, one of the most serious is related to the security of the operating systems. In particular, the official market has shown that is not able to block promptly the publication of malicious software. In this paper we discuss a model checking based approach to detect malware related to Android environment. In the evaluation we focus on the DroidDream threat, a malware able to evade the security mechanism provided by the Android official market, obtaining encouraging results.