期刊名称：International Journal of Security and Its Applications
印刷版ISSN：1738-9976
出版年度：2016
卷号：10
期号：9
页码：193-210
出版社：SERSC
摘要：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.
