Android/Smali semantics in K

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. 

Requirements:

- K tool version 3.5.2.

- Apktool

Instruction:

  • 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/ck.sh path-to-app1.apk path-to-app2.apk

Downloads: