SPARTA: mobile device security

The SPARTA project (Static Program Analysis for Reliable Trusted Apps) is building a toolset to verify the security of mobile phone applications.

SPARTA is a research project funded by the DARPA Automated Program Analysis for Cybersecurity (APAC) program. SPARTA aims to detect certain types of malware in Android applications, or to verify that the app contains no such malware. SPARTA’s verification approach is type-checking: the developer states a security property, annotates the source code with type qualifiers that express that security property, then runs a pluggable type-checker to verify that the type qualifiers are right (and thus that the program satisfies the security property).

In addition to type-checking, SPARTA also provides tools to aide in manual identification of malware in source code. These tools include a tool to show what permissions are needed for each API call used and a tool to report the use of suspicious APIs.

The SPARTA toolset is available from http://types.cs.washington.edu/sparta/. The paper “Collaborative verification of information flow for a high-assurance app store” appeared in CCS 2014.