%0 Journal Article
%T 字节码虚拟机的构造和验证
%A 董渊？
%A 任恺？
%A 王生原？
%A 张素琴？
%J 软件学报
%P 305-317
%D 2010
%X 提出一种虚拟机构造和验证方案.给出字节码程序运行环境bvm(bytecodevirtualmachine)的形式化定义;采用x86机器语言构造虚拟机certvm(certifiedvirtualmachine);并证明该虚拟机实现符合相应程序规范并和bvm之间具有模拟关系.利用辅助工具coq给出证明,所有证明均可机器自动检查.certvm确保在硬件环境满足其语义规范的情况下,已验证的字节码程序能够在给定虚拟机环境中正常运行.给出的方案不仅为虚拟机验证提供理论基础,而且为可信软件构造提供了一种有益的尝试.
%K 已验证虚拟机
%K 模块化验证
%K 字节码
%K 类hoare逻辑
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3794&flag=1