In this paper we propose and implement a provably-correct bytecode verifier for Micro-Dalvik which is a significant subset of Dalvik. We take the approach of a data flow analysis on semilattice to solve the bytecode verification. The operational seman...
In this paper we propose and implement a provably-correct bytecode verifier for Micro-Dalvik which is a significant subset of Dalvik. We take the approach of a data flow analysis on semilattice to solve the bytecode verification. The operational semantics of Micro-Dalvik is developed. The semilattice structure is constructed and transfer functions are defined. Based on the semilattice and transfer functions the well-typing is described. The bytecode verifier is realized to compute a method type to see whether each instruction is assigned a well-typing. By giving conforming relations between the machine state and the well-typing, the correctness of the verifier is proved that the verifier guarantees safe execution and well-typed Micro-Dalvik programs do not produce type errors.