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.
- 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