Logic System for Bytecode Program Modular Certification
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • 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
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 14,2009
  • Revised:July 23,2009
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
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