English Version

Construction and Certification of A Bytecode Virtual Machine
DONG Yuan+, REN Kai, WANG Shengyuan, ZHANG Suqin

Abstract: Virtual Machine (VM), the running environment of bytecode such as JAVA bytecode and .net CIL, is the key technology for hardware- and operating system-independence. Although some efforts have been made on building logic system for bytecode programs, certified programs will still get stuck due to virtual machine fault. To tackle these challenges, this paper presents a method to verify the bytecode programs running environment. The method guarantees that a certified bytecode program will run on the certified VM without getting stuck unless hardware faults occur. We built a certified stack-based virtual machine with this method: we gave the formal definition and the operational semantics of a bytecode machine; we implemented CertVM with X86 assembly code; and we proved that the CertVM is satisfied with the formal definition of our bytecode machine with simulation relation. This system is expressive and fully mechanized. We certified the virtual machine implementation programs in the Coq proof assistant. This work not only provides a solid theoretical foundation for reasoning about virtual machine, but also makes an important advance toward building a certified proof-preserving compiler.

Key words: Certified VM; Program Modular Certification; Bytecode; Hoare-style Logic

中文版本

字节码程序虚拟机的构造和验证
董渊, 任恺, 王生原, 张素琴

摘 要: 语言级虚拟机是平台无关字节码程序的解释执行环境，是当今网络软件和计算设备中广泛使用的重要技术。针对字节码程序和虚拟机平台的程序验证研究，可以提高相关软件的可信程度，具有重要的实用价值和理论价值。虽然近年提出了一系列用于字节码程序的逻辑系统，但是缺乏针对虚拟机实现的可信验证工作。因此即便是已验证字节码程序，一旦虚拟机出错依然无法正确运行。本文给出一种虚拟机构造和验证方案：1）给出字节码程序运行环境BCM（ByteCode Machine）的形式化定义；2）采用机器语言构造虚拟机CertVM（Certified Virtual Machine），并基于FPCC(Foundational Proof-Carrying Code)方法证明该虚拟机符合相应程序规范；3）证明虚拟机的实现程序和BCM之间具有模拟关系，并利用辅助工具Coq给出证明，所有证明均可机器自动检查。CertVM能够确保“硬件环境满足其语义规范的情况下，已验证的字节码程序能够在给定虚拟机环境中正常运行”。本文给出的可信虚拟机构造方案，为广泛使用的一类复杂网络应用程序的深入分析、准确验证和可信运行提供理论帮助，同时为可信软件构造问题的解决提供一种良好思路和有益尝试。

关键词: 已验证虚拟机;模块化验证;字节码;类Hoare逻辑系统

相关链接

Tech. Report: PDF Format
NASAC2009 Slids: PDF Format

---