Program Summary
To be effective, Department of Defense (DoD) cybersecurity solutions require rapid development times. The shelf life of systems and capabilities is sometimes measured in days. Thus, to a greater degree than in other areas of defense, cybersecurity solutions require that DoD develops the ability to build quickly, at scale and over a broad range of capabilities.
DoD has made advances in streamlining its technology acquisition process by taking advantage of commercial off-the-shelf hardware and software. In particular, the commercial mobile application (“apps”) marketplace for smartphones and similar devices holds great potential as a rapid and adaptable supplier for future military software applications, especially as DoD integrates hardened smartphones into its standard equipment for warfighters. The challenge for DoD now becomes validating the security of these apps so that they can be securely and confidently used by warfighters, and doing so on a timeline consistent with operational tempo.
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 will draw 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 will 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.
For APAC to succeed, high-level DoD cybersecurity objectives for mobile apps must be translated into properties that are at a sufficiently low level to be proven with automated program analysis tools. As an example, the generic property, “This application contains no malicious code,” is too high-level to be proven by likely tools. The narrower property, “This Push-to-Talk application is not an eavesdropper,” is still too high-level. The more limited property, “This Push-to-Talk application only records audio when the ‘Talk’ button is pressed,” may be sufficiently low-level to be workable for automated program analysis. APAC will attempt to define many such low-level properties to come closer to DoD’s goal of no malicious code present in its mobile apps marketplaces.
The second challenge APAC aims to address is producing practical, automated tools to demonstrate the cybersecurity properties identified. Successful tools would minimize false alarms, missed detections and the need for human filtering of results to prove properties.
To validate approaches, APAC plans to examine multiple forms of program analysis, including static analysis and hybrid static-dynamic analysis based on symbolic execution. Performers will be broken into Research & Development teams to define properties and create tools and Adversarial Challenge teams to create applications loaded with Trojan horse malicious code using techniques derived from existing Android malware. Performance will be evaluated on the metrics of: rate of false alarms in identifying malicious code, rate of missed detections in identifying malicious code, and human analysis time required.