可信字节码程序虚拟机的构造和验证
虚拟机是平台无关字节码程序的解释执行环境，是当今网络软件和计算设备中广泛使用的重要技术。 针对字节码程序和虚拟机平台的程序验证研究，可以提高相关软件的可信程度，具有重要的实用价值和理论价值。虽然近年提出了一系列用于字节码程序的逻辑系统，但是缺乏针对虚拟机实现的可信验证工作。因此即便是已验证字节码程序，一旦虚拟机出错依然无法正确运行。本文给出一种虚拟机构造和验证方案：1)给出字节码程序运行环境BCM(ByteCode Nachine)的形式化定义：2)采用机器语言构造虚拟机CertVM (Certified VirtualMachine)，并基于FPCC (Foundational Proof-CarryingCode)方法证明该虚拟机符合相应程序规范：3)证明虚拟机的实现程序和BCM之间具有模拟关系，并利用辅助工具Coq给出证明，所有证明均可机器自动检查。CertVM能够确保“只要硬件环境不出问题，已验证的字节码程序能够在给定虚拟机环境中正常运行”。本文给出的可信虚拟机构造方案，为广泛使用的一类复杂网络应用程序的深入分析、准确验证和可信运行提供理论帮助，同时为可信软件构造问题的解决提供一种良好思路和有益尝试。
已验证虚拟机 模块化验证 字节码 类Hoare逻辑系统 网络软件 可信程度
董渊 任恺 王生原 张素琴
清华大学 计算机科学与技术系，北京 100084
国内会议
沈阳
中文
202-213
2009-09-22（万方平台首次上网日期，不代表论文的发表时间）