SymDroid: Symbolic Execution for Dalvik Bytecode

摘要: Apps on Google’s Android mobile device platform are written in Java, but compiled to a special bytecode language called Dalvik. In this paper, we introduce SymDroid, symbolic executor that operates directly Dalvik bytecode. SymDroid begins by first translating into μ-Dalvik, simpler has only 16 instructions, contrast Dalvik’s more than 200 instructions. We present formalism for SymDroid’s executor, which can be described with small number of operational semantics rules; may independent interest. addition modeling also contains models some key portions the platform, including libraries and platform’s lifecycle control code. evaluated two ways. First, ran it Compatibility Test Suite, found passed all tests except ones used library or system routines have not yet implemented. On test suite, runs about twice as slow VM, fast Java VM. Second, discover (path) conditions under contacts accessed an app, was able do so successfully. These results suggest while still prototype, is promising step enabling direct, precise analysis apps.