Principal Investigators: Dr. Eric W. Smith and Dr. Cordell Green
Contributors: Alessandro Coglio and Limei Gilham
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.
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).