%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