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

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

doi:10.1145/3103111.3104040

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 proceeding › Conference proceeding › peer-review

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 language	English
Title of host publication	Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs
Subtitle of host publication	Barcelona, Spain — June 18 - 23, 2017
Publisher	Association for Computing Machinery (ACM)
ISBN (Electronic)	978-1-4503-5098-3
DOIs	https://doi.org/10.1145/3103111.3104040
Publication status	Published - 18 Jun 2017
Event	19th Workshop on Formal Techniques for Java-like Programs - Barcelona, Spain Duration: 18 Jun 2017 → 23 Jun 2017

Workshop

Workshop	19th Workshop on Formal Techniques for Java-like Programs
Country/Territory	Spain
City	Barcelona
Period	18/06/17 → 23/06/17

Access to Document

10.1145/3103111.3104040

Cite this

Software Model Checking: A Promising Approach to Verify Mobile App Security: A Position Paper. / Asăvoae, Irina; Nguyen, Hoang Nga; Roggenbach, Markus et al.

Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs: Barcelona, Spain — June 18 - 23, 2017. Association for Computing Machinery (ACM), 2017. 1.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Asăvoae, I, Nguyen, HN, 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), 19th Workshop on Formal Techniques for Java-like Programs, Barcelona, Spain, 18/06/17. https://doi.org/10.1145/3103111.3104040

@inproceedings{2daf8f7e0bca442b84c101d1181160be,

title = "Software Model Checking: A Promising Approach to Verify Mobile App Security: A Position Paper",

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.",

author = "Irina As{\u a}voae and Nguyen, {Hoang Nga} and Markus Roggenbach and Siraj Shaikh",

year = "2017",

month = jun,

day = "18",

doi = "10.1145/3103111.3104040",

language = "English",

booktitle = "Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "19th Workshop on Formal Techniques for Java-like Programs ; Conference date: 18-06-2017 Through 23-06-2017",

}

TY - GEN

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

AU - Asăvoae, Irina

AU - Nguyen, Hoang Nga

AU - Roggenbach, Markus

AU - Shaikh, Siraj

PY - 2017/6/18

Y1 - 2017/6/18

N2 - 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.

AB - 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.

U2 - 10.1145/3103111.3104040

DO - 10.1145/3103111.3104040

M3 - Conference proceeding

BT - Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs

PB - Association for Computing Machinery (ACM)

T2 - 19th Workshop on Formal Techniques for Java-like Programs

Y2 - 18 June 2017 through 23 June 2017

ER -

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

Abstract

Workshop

Access to Document

Fingerprint

Cite this