  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 appears 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 Kandroid tool, which provides an encoding of the Android/Smali
code semantics within the K framework. Kandroid 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.
