一种用于字节码程序模块化验证的逻辑系统

• 作者: 张丽伟 朱允敏 杨萍 王生原 董渊
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 程序模块化验证 字节码 类Hoare逻辑系统
• 年，卷（期）: 2010,（12）
• 页码范围: 3056-3067
• 分类号: TP301
• 字数: 8071字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2010.03709

摘要

字节码既是运行于虚拟机的解释指令,也是定义良好的中间表示,是当今网络软件和计算设备中广泛使用的重要技术.字节码验证可以提高相关软件的可信程度,同时为构造证明保持编译器提供中间表示支持,具有重要的实用价值和理论价值.虽然近年提出了一些用于字节码程序的逻辑系统,但由于字节码本身的特点,造成了抽象控制栈复杂、控制流结构信息不足,因而字节码程序的"模块化验证"依然是一个巨大的挑战,并没有得到有效解决.将FPCC(foundational proof-carrying code)方法引入中间表示字节码,借鉴汇编程序的验证方法,设计出一种逻辑系统,给出字节码程序运行环境BCM(ByteCode machine)的逻辑系统CBP (certifying bytecode program)定义,完成系统的合理性证明和一组代表性实例程序的模块化证明,并实现机器自动检查.该工作为字节码验证提供一种良好的解决方案,同时也向着构造证明保持编译器环境迈出了坚实的一步,还可以为广泛使用的基于虚拟机复杂网络应用程序的深刻理解和深入分析提供理论帮助.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
2	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
3	杨萍	北京语言大学信息科学学院	5	10	3.0	3.0
4	朱允敏	清华大学计算机科学与技术系	2	12	2.0	2.0
5	张丽伟	清华大学软件学院	3	12	2.0	3.0