Write a Blog >>
Tue 20 Jun 2017 09:30 - 09:50 at Vertex WS217 - A Chair(s): Radu Grigore

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.

Conference Day
Tue 20 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
AFTfJP at Vertex WS217
Chair(s): Radu GrigoreUniversity of Kent
09:30
20m
Talk
Software Model Checking: A Promising Approach to Verify Mobile App Security
FTfJP
Irina AsavoaeINRIA, Paris, France, Hoang Nga NguyenCoventry University, Coventry, UK, Markus RoggenbachSwansea University, Swansea, UK, Siraj Ahmed ShaikhCoventry University, Coventry, UK
Pre-print
09:50
35m
Talk
Formal Analysis of Object-Oriented Mograms
FTfJP
Moussa AmraniUniversity of Namur, Pierre Yves SchobbensUniversity of Namur
10:25
5m
Talk
Towards a Java Subtyping Operad
FTfJP
Moez A. AbdelGawadInformatics Research Institute, SRTA-City, Alexandria, Egypt
Pre-print