---

Download: PDF.

“Collaborative verification of information flow for a high-assurance app store” by M. D. Ernst, R. Just, S. Millstein, W. Dietl, S. Pernsteiner, F. Roesner, K. Koscher, P. Barros, R. Bhoraskar, S. Han, P. Vines, and E. X. Wu. In Computer and Communications Security (CCS), Nov. 2014, pp. 1092-1104.

Abstract

Current app stores distribute some malware to unsuspecting users, even though the app approval process may be costly and time-consuming. We propose the creation of high-integrity app stores that provide certain guarantees to their customers. Our approach has four key features. (1) Our analysis is based upon a flow-sensitive, context-sensitive information-flow type system. (2) We use finer-grained behavioral specifications of information flow than current app stores, along with automated analysis to prove correctness with respect to the specification. (3) Our approach works on source code rather than binaries and is based on formal verification rather than on bug-finding. (4) We use a collaborative verification methodology in which the software vendor and the app store auditor each do tasks that are easy for them, reducing overall cost.

We have implemented our system for Android apps written in Java. In an adversarial Red Team evaluation, we were given 72 apps (576,000 LOC) to analyze for malware. The 57 Trojans among these had been written specifically to defeat a malware analysis such as ours, and the Red Teams had access to our source code and documentation. Nonetheless, our information-flow type system was effective: it detected 96% of malware whose malicious behavior was related to information flow and 82% of all malware. In practice our toolset would be combined with other analyses to reduce the chance of approving a Trojan. The programmer annotation burden is low: 6 annotations per 100 lines of code. Every sound analysis requires a human to review potential false alarms, and in our experiments, this took 30 minutes per KLOC for an auditor unfamiliar with the app.

Keywords: Android, information flow security, type system

Download: PDF.

BibTeX entry:

@inproceedings{infoflow-ccs2014,
   author = {M. D. Ernst and R. Just and S. Millstein and W. Dietl and S.
        Pernsteiner and F. Roesner and K. Koscher and P. Barros and R.
        Bhoraskar and S. Han and P. Vines and E. X. Wu},
   title = {Collaborative verification of information flow for a
        high-assurance app store},
   booktitle = {Computer and Communications Security (CCS)},
   month = nov,
}

---

---