SPARTA!

Static Program Analysis for Reliable Trusted Apps

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.

• Download:
  • SPARTA Toolset version 1.0.2, 3 February 2016
  • SPARTA VM version 1.0.0, 28 Dec 2014
  • Sample apps
  • Previous releases
• Documentation:
  • SPARTA Manual (PDF)
  • SPARTA Manual (HTML)
• Source code repository (at GitHub): https://github.com/typetools/sparta/
  
• Research papers:
  • “Collaborative verification of information flow for a high-assuranceq app store” by Michael D. Ernst, René Just, Suzanne Millstein, Werner M. Dietl, Stuart Pernsteiner, Franziska Roesner, Karl Koscher, Paulo Barros, Ravi Bhoraskar, Seungyeop Han, Paul Vines, and Edward X. Wu. In Proceedings of the 21st ACM Conference on Computer and Communications Security, (Scottsdale, AZ, USA), November 4-6, 2014.
    Download (PDF). Apps used in Usabilty Study. Virtual Machine with the verision of IFC used in the paper installed.

  • “Static analysis of implicit control flow: Resolving Java reflection and Android intents”
    by Paulo Barros, René Just, Suzanne Millstein, Paul Vines, Werner Dietl, Marcelo d'Amorim, and Michael D. Ernst.
    In ASE 2015: Proceedings of the 30th Annual International Conference on Automated Software Engineering, (Lincoln, NE, USA), November 11-13, 2015.
    Details. Download: PDF, slides (PDF), slides (PowerPoint), extended version.
    An extended version appeared as “Static analysis of implicit control flow: Resolving Java reflection and Android intents (extended version)” by Paulo Barros, René Just, Suzanne Millstein, Paul Vines, Werner Dietl, Marcelo d'Amorim, and Michael D. Ernst. University of Washington Department of Computer Science and Engineering technical report UW-CSE-15-08-01, (Seattle, WA, USA), Aug. 2015.
    A previous version appeared as University of Washington Department of Computer Science and Engineering technical report UW-CSE-15-05-01, (Seattle, WA, USA), May 2015.

Mailing lists

We welcome questions, suggestions, pull requests, reports about case studies, and other contributions.

• sparta@cs.washington.edu: to reach the developers who maintain and extend the SPARTA toolset
• sparta-users: for general discussion about the SPARTA toolset

Bug reports

To submit a bug report, use the mailing list or, preferably, the issue tracker:

• SPARTA toolset issue tracker

Last updated: April 15, 2016