一种用于字节码程序模块化验证的逻辑系统
基金项目:

Supported by the National Natural Science Foundation of China under Grant Nos.90818019, 90816006 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant Nos.2008AA01Z102, 2009AA011902 (国家高技术研究发展计划(863))

  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [31]
  • |
  • 相似文献
  • | | |
  • 文章评论
    摘要:

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

    Abstract:

    Bytecode, which is widely used in network software and mass devices, is a kind of interpretive execution instruction and a favorable intermediate presentation, Bytecode can highly improve the reliability of relevant software and strongly support the construction of proof-preserved compilers, so it holds theoretical and practical value. Although some efforts have been made on building a logic system for the bytecode program, modular certification of bytecode still remains challenging because of the complexity of the abstract control stack and the lack of control over flow structure information. Moreover, the expression ability of the recent logic system is very limited. This paper presents a logic framework that supports modular certification of bytecode programs and is more expressive. FPCC technology is originally introduced into this framework for bytecode. This paper provides the formal definition of CBP (certifying bytecode program) logic system for the running environment of Bytecode. Also, this paper has also finished the proof of the theorem and a group of instance programs. This piece of work is not only a good solution for certifying Bytecode, which is run on a stack-based virtual machine, but also a significant improvement for the construction of a proof-preserved compiler environment. In addition, this system is useful in finding a deeper understanding and analysis of network application based on a virtual machine.

    参考文献
    [1] Hoare T. The verifying compiler: A grand challenge for computing research. Journal of the ACM, 2003,50(1):63?69. [doi: 10.1145/602382.602403]
    [2] Hall M, Padua D, Pingali K. Compiler research: The next 50 years. Communications of the ACM, 2009,52(2):60?67.
    [3] Lindholm T, Yellin F. The Java Virtual Machine Specification. 2nd ed., Prentice Hall PTR, 1999.
    [4] ECMA. Standard ECMA-335 Common Language Infrastructure. 4th ed., 2006.
    [5] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009,52(7):107?115. [doi: 10.1145/1538788. 1538814]
    [6] Necula GC, Lee P. The design and implementation of a certifying compiler. In: Proc. of the Conf. on Programming Language Design and Implementation. New York: ACM Press, 1998. 333?344. http://portal.acm.org/citation.cfm?id=277752
    [7] Appel AW. Foundational proof-carrying code. In: Proc. of the 16th IEEE Symp. on Logic in Computer Science. IEEE Computer Society, 2001. 247?258. http://portal.acm.org/citation.cfm?id=871860
    [8] Yu DC, Hamid NA, Shao Z. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 2004,50(1-3):101?127. [doi: 10.1016/j.scico.2004.01.003]
    [9] Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In: Proc. of the Conf. on Programming Language Design and Implementation (PLDI 2006). New York: ACM Press, 2006. 401?414. http://portal.acm.org/citation.cfm?id=1133981.1134028
    [10] Cai HX, Shao Z, Vaynberg A. Certified self-modifying code. In: Proc. of the Conf. on Programming Language Design and Implementation (PLDI 2007). New York: ACM Press, 2007. 66?77. http://portal.acm.org/citation.cfm?id=1250743
    [11] Feng X, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. In: Proc. of the Conf. Programming Language Design and Implementation (PLDI 2008). New York: ACM Press, 2008. 170?182. http://portal.acm.org/citation.cfm?id=1375581.1375603
    [12] Wang SY, Dong Y. A verifiable low-level concurrent programming model based on colored Petri nets. In: Sidorova N, Moldt D, Rolke H, eds. Proc. of the Petri Nets and Distributed Systems 2008. 2008. 23?24.
    [13] Leroy X. Bytecode verification for Java smart card. Software Practice & Experience, 2002,32:319?340.
    [14] Quigley CL. A programming logic for java bytecode programs. In: Basin D, Wolff B, eds. Proc. of the 16th Int’l Conf. on Theorem Proving in Higher-Order Logics (TPHOLs 2003). Berlin: Springer-Verlag, 2003. 41?54.
    [15] Aspinall D, Beringer L, Hofmann M, Loidl HW, Momigliano A. A program logic for resource verification. In: Slind K, et al., eds. Proc of the 17th Int’l Conf. on Theorem Proving in Higher-Order Logics (TPHOLs 2004). Berlin: Springer-Verlag, 2004. 34?49.
    [16] Bannwart F, Muller P. A program logic for bytecode. Electronic Notes in Theoretical Computer Science. Elsevier, 2005,141(1): 255?273.
    [17] Benton N. A typed, compositional logic for a stack-based abstract machine. In: Proc. of the 3rd Asian Symp. on Programming Languages and Systems (APLAS). Springer-Verlag, 2005. 364?380. http://www.springerlink.com/index/f410033626518g70.pdf
    [18] Burdy L, Pavlova M. Java bytecode specification and verification. In: Proc. of the Symp. on Applied Computing. New York: ACM Press, 2006. 1835?1839. http://portal.acm.org/ft_gateway.cfm?id=1141708&type=pdf
    [19] Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.1, 2006.
    [20] Dong Y, Wang SY, Zhang LW, Zhu YM, Yang P. Modular certification of bytecode programs. 2009. http://soft.cs.tsinghua.edu.cn/ dongyuan/~dongyuan/verify/cbp.html
    [21] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969,26(1):53?56. [doi: 10.1145/357980.358001]
    [22] Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science (LICS 2002). IEEE Computer Society, 2002. 55?74. http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber= 1029817
    [23] Weiss M, de Ferrire F, Delsart B, Fabre C, Hirsch F, Johnson EA, Joloboff V, Roy F, Siebert F, Spengler X. Turboj, a Java bytecode-to-native compiler. In: Proc. of the Conf. on Language, Compilers and Tools for Embedded Systems. Beilin: Springer-Verlag, 1998. 119?130. http://portal.acm.org/citation.cfm?id=710493
    [24] Sen K. Race directed randomized dynamic analysis of concurrent programs. In: Proc. of the Conf. on Programming Language Design and Implementation (PLDI 2007). New York: ACM Press, 2008. 11?21. http://portal.acm.org/citation.cfm?id=1375584
    [25] Dong Y, Wang SY, Zhang LW, Yang P. Modular certification of low-level intermediate representation programs. In: Ahamed SI, et al., eds. Proc. of the 33rd Annual IEEE Int’l Computer Software and Applications Conf. (COMPSAC 2009). IEEE Computer Society, 2009. 563?570.
    [26] Zhu YM, Zhang LW, Wand SY, Dong Y, Zhang SQ. Verjfying parallel low-level programs for multi-core processor. ACTA ELEClRONICA SINICA, 2009,37(4A):1?6 (in Chinese with English abstract).
    [27] Chen YY, Hua BJ, Ge L, Wang ZF. A pointer logic for safety verification of pointer programs. Chinese Journal of Computers, 2008, 31(3):372?380 (in Chinese with English abstract).
    [28] Guo Y, Chen YY, Lin CX. A method for code safety proof construction. Journal of Software, 2008,19(10):2720?2727 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/19/2720.htm [doi: 10.3724/SP.J.1001.2008.02720]
    附中文参考文献: [26] 朱允敏,张丽伟,王生原,董渊,张素琴.面向多核处理器的低级并行程序验证.电子学报.2009,37(4A):1?6.
    [27] 陈意云,华保健,葛琳,王志芳.一种用于指针程序安全性证明的指针逻辑.计算机学报,2008,31(3):372?380.
    [28] 郭宇,陈意云,林春晓.一种构造代码安全性证明的方法.软件学报,2008,19(10):2720?2727. http://www.jos.org.cn/1000-9825/ 2720.htm [doi: 10.3724/SP.J.1001.2008.02720]
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

董渊,王生原,张丽伟,朱允敏,杨萍.一种用于字节码程序模块化验证的逻辑系统.软件学报,2010,21(12):3056-3067

复制
分享
文章指标
  • 点击次数:4423
  • 下载次数: 6735
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2009-03-14
  • 最后修改日期:2009-07-23
文章二维码
您是第19986226位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号