Android/Smali semantics in K

Error message

Deprecated function: The each() function is deprecated. This message will be suppressed on further calls in menu_set_active_trail() (line 2375 of /compsci/partition2/csmarkus/public_html/ProcessesAndData/includes/

Kandroid is an implementation of Android/Smali code semantics in the K framework, supported by ACID project. The aim of Kandroid is to provide a Formal-Methods based platform to detect colluding Android applications. There are two implementations: concrete and abstract. The concrete version implements the semantics of Smali instructions as specified on Android Project website. In contrast to that, the abstract one focuses on capturing the data-flow required to decide if collusion happens. Here, the concrete semantics serves a point of reference, in order to control the abstraction. 


- K tool version 3.5.2.

- Apktool


  • Add the path to kompile and krun of K tool to the environment variable PATH in your system.
  • For the concrete version, the following instruction is for OSX:
    • to compile, run: script/akom
    • to run model check: script/ path-to-app1.apk path-to-app2.apk