Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover

Presented as part of the 2016 HCSS conference.

ABSTRACT

We present our work in using the ACL2 theorem prover to formally model the Android platform and to formally verify Android apps. Our approach allows the verification of the full functional correctness of apps (e.g., that a calculator app computes the correct numeric result) as well as security properties (e.g., that an app only sends data to certain URLs).  Verifying an app with our system provides high assurance that it satisfies its specification.  A major motivation for this work is to detect or prove the absence of ``functional malware'', malicious app functionality that is triggered by complex conditions on state and whose malicious action is to cause the app to calculate the wrong results or otherwise behave incorrectly, unbeknown to the user.

Android is an event-driven system.  Our formal model is an executable simulator of a growing subset of the Android platform, and app proofs are done by automated symbolic execution of the app's event handlers using the formal model.  By induction, we prove that an app satisfies an invariant, including the correctness properties of interest, for all possible sequences of events.  To our knowledge, our formal Android model is the most detailed and our Android app verification is the most thorough, compared to other approaches.

BIO

Dr. Eric W. Smith is a Senior Computer Scientist at Kestrel Institute with 15 years of experience in formal methods. He currently leads Kestrel's DARPA MUSE effort, which uses synthesis techniques (derivations, specifications, and refinements) to construct correctness proofs of code found in large online repositories. This allows the code to be soundly used in program synthesis. He also leads Kestrel's DARPA APAC effort to find malware in Android apps or formally prove its absence. Dr. Smith has applied Kestrel's Specware system for software synthesis in various domains for DoD customers. This work included producing machine-checkable proofs of correctness in the Isabelle/HOL theorem prover.  He is currently leading a project to bring Specware-like synthesis capabilities to the ACL2 theorem prover.

Before joining Kestrel, Dr. Smith completed his Ph.D. in Computer Science at Stanford University under Prof. David Dill. He wrote Axe, a theorem prover and equivalence checker capable of highly automated proofs about real-world cryptographic programs. Dr. Smith has extensive experience with the ACL2 theorem prover, using it for microprocessor verification at AMD and for processor modeling and machine code proofs at Rockwell Collins.  Dr. Smith did his undergraduate work at the University of Texas at Austin, where he earned bachelor's degrees in Computer Science and Plan II Honors under thesis advisor J Moore.