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

• 作者: 任恺 张素琴 王生原 董渊
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 已验证虚拟机 模块化验证 字节码 类Hoare逻辑
• 年，卷（期）: 2010,（2）
• 页码范围: 305-317
• 页数: 13页
• 分类号: TP316
• 字数: 8997字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张素琴	清华大学计算机科学与技术系	43	714	14.0	26.0
2	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
3	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
4	任恺	清华大学计算机科学与技术系	1	8	1.0	1.0