Software Model Checking: A Promising Approach to Verify Mobile App Security: A Position Paper

Irina Asăvoae, Hoang Nga Nguyen, Markus Roggenbach, Siraj Shaikh

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

2 Citations (Scopus)

Abstract

In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion is when, in performing a threat, several apps are working together, i.e., they exchange information which they could not obtain on their own. In this context, we developed the K-Android tool, which provides an encoding of the Android/Smali code semantics within the K framework. K-Android allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems.
Original languageEnglish
Title of host publicationProceedings of the 19th Workshop on Formal Techniques for Java-like Programs
Subtitle of host publicationBarcelona, Spain — June 18 - 23, 2017
PublisherAssociation for Computing Machinery (ACM)
ISBN (Electronic)978-1-4503-5098-3
DOIs
Publication statusPublished - 18 Jun 2017
Event19th Workshop on Formal Techniques for Java-like Programs - Barcelona, Spain
Duration: 18 Jun 201723 Jun 2017

Workshop

Workshop19th Workshop on Formal Techniques for Java-like Programs
CountrySpain
CityBarcelona
Period18/06/1723/06/17

Fingerprint Dive into the research topics of 'Software Model Checking: A Promising Approach to Verify Mobile App Security: A Position Paper'. Together they form a unique fingerprint.

  • Cite this

    Asăvoae, I., Nguyen, H. N., Roggenbach, M., & Shaikh, S. (2017). Software Model Checking: A Promising Approach to Verify Mobile App Security: A Position Paper. In Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs: Barcelona, Spain — June 18 - 23, 2017 [1] Association for Computing Machinery (ACM). https://doi.org/10.1145/3103111.3104040