Application marketplaces (such as the Android Market) provide users with a wide range of desirable applications for their mobile devices. But application marketplaces can also provide a compelling distribution channel for attackers who place attractive applications containing malware into the application marketplace.
The Provably Safe Android Apps project is developing a static program analysis system for finding malware in Android applications written in Java. A goal is ensuring that application marketplaces contain only safe mobile applications.
As part of this effort we are developing techniques to statically verify that Android applications never violate key security properties. Given a specification that identifies the operating modes of the application and the sequences of safe operations in each mode, the analysis determines if the application satisfies the specification. If it does not, it automatically modifies the application so that it does. Once again, the goal is to preserve as much of the desirable functionality of the application as possible while ensuring that the system remains secure.