You are now leaving the website that is under the control and management of DARPA. The appearance of hyperlinks does not constitute endorsement by DARPA of non-U.S. Government sites or the information, products, or services contained therein. Although DARPA may or may not use these sites as additional distribution channels for Department of Defense information, it does not exercise editorial control over all of the information that you may find at these locations. Such links are provided consistent with the stated purpose of this website.

After reading this message, click to continue immediately.

Go Back

/ Information Innovation Office (I2O)

Automated Program Analysis for Cybersecurity (APAC)

The Automated Program Analysis for Cybersecurity (APAC) program aims to address the challenge of timely and robust security validation of mobile apps by first defining security properties to be measured against and then developing automated tools to perform the measuring. APAC draws heavily from the field of formal-methods program analysis (theorem proving, logic and machine proofing) to keep malicious code out of DoD Android-based application marketplaces. APAC seeks to apply recent research breakthroughs in this field in an attempt to scale DoD's program analysis capability to a level never before achieved with an automated solution.

Program Complete

The content below has been generated by organizations that are partially funded by DARPA; the views and conclusions contained therein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of DARPA or the U.S. Government.

Report a problem:

Last updated: November 13, 2015

MIT (publications), Kestrel Institute (publications), GITI (publications) DroidSafe Infrastructure The DroidSafe static analysis tool produces a security summary of Android applications to help trusted parties rapidly understand sensitive behaviors of a untrusted application. The core analysis is flow, object, event, and value sensitive. The results are presented in a graphic user interface tied to source code for inspection. (Java/Python) LGPL
BAE Systems (publications) Droid Reasoning, Analysis, and Protection Engine (DRAPE) Software, Dynamic Analysis, Android, Malware Not Ready for Release DRAPE brings together concolic execution, taint analysis and execution path clustering to analyze Android applications. DRAPE will elicit stealthy malware that is triggered under specific conditions, and will provide the analyst with a characterization of those conditions. (Java)
University of Washington (publications) Checker Framework Static analysis The Checker Framework enhances Java's type system to make it more powerful and useful. This lets software developers detect and prevent errors in their Java programs. (Java) GPLv2
University of Washington (publications) Type annotations compiler Static analysis, Compilers Java 8 will include support for type annotations. The Type Annotations compiler (also called the JSR 308 compiler) is fully backward-compatible. You can use it in place of javac (for Java 8) without any change in behavior, except that you will be permitted to write annotations in comments. This lets you write type annotations, but keep your code compilable by Java 4/5/6/7 compilers. (Java) GPLv2
University of Washington (publications) Annotation File Utilities Java Annotation Tool Tools for reading annotations from, and inserting type annotations in, Java source and class files. (Java) MIT
University of Washington (publications) SPARTA Toolset Static analysis, Android, Security 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). (Java) GPLv2
University of Washington JavaUI: Effects for Controlling UI Object Access
University of Washington Rely-Guarantee References for Refinement Types Over Aliased Mutable Data
University of Washington ReIm & ReImInfer: Checking and Inference of Reference Immutability and Method Purity
BAE Systems Automated Execution Control and Dynamic Behavior Monitoring for Android Applications
BAE Systems Behavior Analysis via Execution Path Clusters
MIT, Kestrel Institute, GITI Contextual Policy Enforcement in Android Applications with Permission Event Graphs