원문정보
초록
영어
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.
목차
1. Introduction
2. The Operational Semantics of Micro-Dalvik
2.1. The Micro-Dalvik Instructions and Programs
2.2. The Operational Semantics of Micro-Dalvik
3. Type System for Micro-Dalvik
3.1. A Concrete Example
3.2. A Basic Semilattice Structure
3.3. Semilattice Construction for Micro-Dalvik’s State Type
3.4. Transfer functions of Micro-Dalvik
3.5. Well-typings of Micro-Dalvik
4. Type Inference and Type Safety
5. Related Work
6. Conclusion
Acknowledgments
References