字节码虚拟机的构造和验证

提出一种虚拟机构造和验证方案.给出字节码程序运行环境bvm(bytecodevirtualmachine)的形式化定义;采用x86机器语言构造虚拟机certvm(certifiedvirtualmachine);并证明该虚拟机实现符合相应程序规范并和bvm之间具有模拟关系.利用辅助工具coq给出证明,所有证明均可机器自动检查.certvm确保在硬件环境满足其语义规范的情况下,已验证的字节码程序能够在给定虚拟机环境中正常运行.给出的方案不仅为虚拟机验证提供理论基础,而且为可信软件构造提供了一种有益的尝试.