Earticle

초록

영어

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.

목차

Abstract
 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

키워드

저자

• Jiang Nan [ Computer School, Wuhan University, China, Computer School, Hubei University of Technology, China ] Corresponding author
• He Yanxiang [ Computer School, Wuhan University, China, State Key Laboratory of Software Engineering (Wuhan University), China ]
• Zhang Xiaotong [ Computer School, Wuhan University, China ]
• Liu Rui [ Computer School, Wuhan University, China ]
• Shen Yunfei [ Computer School, Wuhan University, China ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Security and Its Applications

• 간기

  격월간

• pISSN

  1738-9976

• 수록기간

  2008~2016

• 등재여부

  SCOPUS

• 십진분류

  KDC 505 DDC 605