Software Model Checking: A Promising Approach to Verify Mobile App Security
In this position paper we advocate software model check- ing as a technique suitable for security of analysis mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. To this end we devel- oped 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.
Tue 20 Jun Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|09:30 - 09:50|
Irina AsavoaeINRIA, Paris, France, Hoang Nga NguyenCoventry University, Coventry, UK, Markus RoggenbachSwansea University, Swansea, UK, Siraj Ahmed ShaikhCoventry University, Coventry, UKPre-print
|09:50 - 10:25|
|10:25 - 10:30|
Moez A. AbdelGawadInformatics Research Institute, SRTA-City, Alexandria, EgyptPre-print