English Version

A Logic System for Bytecode Modular Certification
DONG Yuan, WANG Shengyuan, ZHANG Liwei, ZHU Yunmin , YANG Ping

Abstract: Bytecode is a kind of interpretive execution instruction and a favorable intermediate presentation, which is widely used in network software and mass device. The work of certifying Bytecode can highly improve the reliability of relevant software and strongly support the construction of proof-preserved compiler, so it is of important theoretical value and practical value. Although some efforts have been made on building logic system for bytecode program, modular certification of bytecode still remains challenging because of the complexity of abstract control stack and the lack of control flow structure information. Moreover, most recent logic system’s expression ability is much limited. In this paper, we present a new logic framework which supports modular certification of bytecode programs and is more expressive, and FPCC technology is originally introduced into our framework for bytecode. We provide the formal definition of CBP(Certifying Bytecode Program) logic system for the running environment of Bytecode. Also, we have finished the proof of the soundness theorem and a group of instance programs. Our work is not only a good solution for certifying Bytecode which is run on stack-based virtual machine but also a significant improvement for the construction of proof-preserved compiler environment. In addition, our system is useful for deeper understanding and analysis of network application based on virtual machine.

Key words: Program Modular Certification; Bytecode; Hoare-like Logic

中文版本

一种用于字节码程序模块化验证的逻辑系统
董渊, 王生原, 张丽伟, 朱允敏, 杨 萍

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

关键词: 程序模块化验证;字节码;类 Hoare 逻辑系统

相关链接

Tech. Report: PDF Format
技术报告: PDF Format

---