Konferenzbeitrag
Collaborative verification of information flow for a high-assurance app store
Lade...
Volltext URI
Dokumententyp
Text/Conference Paper
Dateien
Zusatzinformation
Datum
2015
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
Current app stores distribute some malware to unsuspecting users, even though the app approval process may be costly and time-consuming. High-integrity app stores must provide stronger guarantees that their apps are not malicious. This talk presents a verification model for use in such app stores to guarantee that the apps are free of malicious information flows. In this model, the software vendor and the app store auditor collaborate-each does tasks that are easy for her/him, reducing overall verification cost. The software vendor provides a behavioral specification of information flow and source code annotated with information-flow type qualifiers. This talk also presents our flow-sensitive, context-sensitive information-flow type system that checks those information flow type qualifiers and proves that only information flows in the specification can occur at run time. We have implemented the information-flow type system for Android apps written in Java, and we evaluated both its effectiveness and usability in practice. In an adversarial Red Team evaluation, we analyzed 72 apps (576,000 lines of code) for malware. Our information-flow type system was effective: it detected 96\% of malware whose malicious behavior was related to information flow.