Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/141484
Full metadata record
DC FieldValueLanguage
dc.contributor.authorBai, Guangdongen_US
dc.contributor.authorYe, Quanqien_US
dc.contributor.authorWu, Yongzhengen_US
dc.contributor.authorBotha, Heilaen_US
dc.contributor.authorSun, Junen_US
dc.contributor.authorLiu, Yangen_US
dc.contributor.authorDong, Jin Songen_US
dc.contributor.authorVisser, Willemen_US
dc.date.accessioned2020-06-08T16:05:06Z-
dc.date.available2020-06-08T16:05:06Z-
dc.date.issued2018-
dc.identifier.citationBai, G., Ye, Q., Wu, Y., Botha, H., Sun, J., Liu, Y., . . ., Visser, W. (2018). Towards model checking android applications. IEEE Transactions on Software Engineering, 44(6), 595 - 612. doi:10.1109/TSE.2017.2697848en_US
dc.identifier.issn0098-5589en_US
dc.identifier.urihttps://hdl.handle.net/10356/141484-
dc.description.abstractAs feature-rich Android applications (apps for short) are increasingly popularized in security-sensitive scenarios, methods to verify their security properties are highly desirable. Existing approaches on verifying Android apps often have limited effectiveness. For instance, static analysis often suffers from a high false-positive rate, whereas approaches based on dynamic testing are limited in coverage. In this work, we propose an alternative approach, which is to apply the software model checking technique to verify Android apps. We have built a general framework named DroidPF upon Java PathFinder (JPF), towards model checking Android apps. In the framework, we craft an executable mock-up Android OS which enables JPF to dynamically explore the concrete state spaces of the tested apps; we construct programs to generate user interaction and environmental input so as to drive the dynamic execution of the apps; and we introduce Android specific reduction techniques to help alleviate the state space explosion. DroidPF focuses on common security vulnerabilities in Android apps including sensitive data leakage involving a non-trivial flow- and context-sensitive taint-style analysis. DroidPF has been evaluated with 131 apps, which include real-world apps, third-party libraries, malware samples and benchmarks for evaluating app analysis techniques like ours. DroidPF precisely identifies nearly all of the previously known security issues and nine previously unreported vulnerabilities/bugs.en_US
dc.description.sponsorshipNRF (Natl Research Foundation, S’pore)en_US
dc.language.isoenen_US
dc.relation.ispartofIEEE Transactions on Software Engineeringen_US
dc.rights© 2018 IEEE. All rights reserved.en_US
dc.subjectEngineering::Computer science and engineeringen_US
dc.titleTowards model checking android applicationsen_US
dc.typeJournal Articleen
dc.contributor.schoolSchool of Computer Science and Engineeringen_US
dc.identifier.doi10.1109/TSE.2017.2697848-
dc.identifier.scopus2-s2.0-85048698844-
dc.identifier.issue6en_US
dc.identifier.volume44en_US
dc.identifier.spage595en_US
dc.identifier.epage612en_US
dc.subject.keywordsSoftware Model Checkingen_US
dc.subject.keywordsSecurity Verificationen_US
item.grantfulltextnone-
item.fulltextNo Fulltext-
Appears in Collections:SCSE Journal Articles

SCOPUSTM   
Citations 20

21
Updated on Jan 28, 2023

Web of ScienceTM
Citations 20

16
Updated on Jan 30, 2023

Page view(s)

141
Updated on Feb 4, 2023

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.