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.

Tue 20 Jun

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

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