APAC Project

Principal Investigators: Dr. Eric W. Smith and Dr. Cordell Green

Contributors: Alessandro Coglio and Limei Gilham

Objective:

The DARPA APAC (Automated Program Analysis for Cybersecurity) program aims to develop sound tools to analyze Android applications for malware. In particular, the goal is to keep malware off of the phones and other mobile devices. Kestrel is working with MIT and GITI to develop Droidsafe, a sound static analyzer capable of checking applications for conformance with a security specification (indicating which security-critical API calls are allowed in response to which input events). Kestrel is also using the ACL2 theorem prover to formally verify full functional correctness of Android apps to exclude malware based on subtle functional deviations.

Publications:

Eric Smith and Alessandro Coglio. Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover. 7th Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE). July 2015.