• Article
  • | |
  • Metrics
  • |
  • Reference [31]
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    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.

    Reference
    [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]
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:4413
  • PDF: 6464
  • HTML: 0
  • Cited by: 0
History
  • Received:March 14,2009
  • Revised:July 23,2009
You are the first2038183Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063