This project is developing tools and techniques for cost-effective evaluation of the trustworthiness of mobile applications (apps). The work focuses on enterprise scenarios, in which personnel at a business or government agency use mission-related apps and access enterprise networks.

In such scenarios there are incentives and resources for much more substantive evaluations and controls on information flow than are currently found in commodity app marketplaces. The project aims to advance the science needed for static techniques to be usable by professional development and evaluation teams and useful for achieving dramatically improved assurance. The project's goals are to: (a) find flexible and expressive ways to specify information flow requirements for apps, (b) find effective ways to specify what is assumed about the Android platform, and (c) find practical static analysis and verification techniques to check security of apps with respect to given policies and the platform. Results include specification techniques and theory - models and algorithms. These are applied in case studies with prototype tools that the project develops, to evaluate how well the goals are achieved.

The project's techniques can be deployed by certification organizations to provide scientifically sound techniques for assurance, thus enabling the full benefits of highly-integrated mobile software in mission-critical situations. Software designers will benefit from being able to precisely specify end-to-end requirements as well as component interfaces. Software developers will benefit from reliable means to detect design flaws and bugs, malware in third-party software, and unintended functionality that exposes vulnerabilities. Beyond the specific target of mobile software, the techniques will be of use in other settings, especially web applications, where it is crucial to reason about interfaces between mutually untrusting parties making heavy use of callbacks. The project could help improve security in government agencies and private sector, indirectly benefitting national security and the general population.