You are now leaving the DARPA.mil 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.
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.
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: firstname.lastname@example.org
Last updated: November 13, 2015
|MIT (publications), Kestrel Institute (publications), GITI (publications)||DroidSafe||Infrastructure||https://github.com/mgordon/droidsafe.git||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||https://code.google.com/p/checker-framework/||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||https://code.google.com/p/jsr308-langtools/||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||https://code.google.com/p/annotation-tools/||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||http://types.cs.washington.edu/sparta/release/||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||http://homes.cs.washington.edu/~mernst/pubs/gui-thread-ecoop2013.pdf|
|University of Washington||Rely-Guarantee References for Refinement Types Over Aliased Mutable Data||http://homes.cs.washington.edu/~mernst/pubs/rely-guarantee-ref-pldi2013.pdf|
|University of Washington||ReIm & ReImInfer: Checking and Inference of Reference Immutability and Method Purity||http://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-oopsla2012.pdf|
|BAE Systems||Automated Execution Control and Dynamic Behavior Monitoring for Android Applications||http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6735749&url=http%3A%2F%2Fieeexplore.ieee.org%2Fstamp%2Fstamp.jsp%3Ftp%3D%26arnumber%3D6735749|
|BAE Systems||Behavior Analysis via Execution Path Clusters||http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6735750&url=http%3A%2F%2Fieeexplore.ieee.org%2Fstamp%2Fstamp.jsp%3Farnumber%3D6735750|
|MIT, Kestrel Institute, GITI||Contextual Policy Enforcement in Android Applications with Permission Event Graphs||http://www.internetsociety.org/sites/default/files/06_4_0.pdf|