一种用于指针程序安全性证明的指针逻辑
|
摘要
在社会逐渐走入信息时代的今天,社会的各个层面,包括工业界、政府机关、学校、商业部门等,都和计算机软件等信息系统结合越来越紧密。信息系统中的任何一个环节工作失败或是遭受攻击都会带来难以预料的灾难性后果,因而软件安全的重要性与日俱增。用形式化的方法对软件进行严格推理是提高软件质量的根本途径。在众多的形式化方法中,近十年来基于程序设计语言理论和实现技术的软件安全研究引起了广泛的关注。基于语言理论的研究从程序基础出发考虑软件安全,有利于减小运算系统的受信任计算基础(TrustedComputing Base,简称TCB)。
未来高安全软件设计和开发的一种行之有效的方式将是基于程序性质证明的开发框架。在这个框架中,程序设计者将软件的安全策略等描述成程序应满足的规范,连同程序一起提交给编译器:编译器生成为证明程序满足规范所需的验证条件,并且利用内嵌的定理证明器自动地或交互地证明这些验证条件;编译器在把源程序翻译成目标代码的同时,将源程序满足规范的证明翻译成目标代码满足等效规范的证明,这样的编译器称为出具证明的编译器(certifyingcompiler);在目标代码一级由证明检验器利用代码所携带的证明自动进行代码满足规范的检验。该框架的主要优点是,它向程序设计者提供源级而不是目标级的程序性质证明方法,以提高安全程序的开发效率,同时它将编译器、证明器等排除出受信任的计算基础,以尽量缩小系统的TCB。
作为上述基于程序性质证明的软件安全长期研究工作的一个环节和组成部分,本文在指针逻辑以及基于指针逻辑的源代码性质描述和性质证明方面做了有益探索。
本文首先研究了一个强调指针类型的类C的命令式语言源语言PointerC的设计并给出了它的安全性证明。PointerC语言设计的主要出发点是:已有软件安全和出具证明编译的研究大多集中在类型安全等简单安全策略上;而本文研究的高安全程序设计框架关注更实际、更丰富的安全策略,如内存安全等,因此,PointerC保留了C语言指针特性。本文给出了一种易于程序员理解的安全语言描述方式,并尝试以类型系统和逻辑系统相结合的静态机制来推理程序的安全性。本文利用辅助定理证明工具Coq,机械证明了PointerC语言的安全性定理。
本文研究了一种指针逻辑系统。指针逻辑扩展了传统Hoare逻辑,并加入了新的推理规则以支持对指针操作的推理,因此指针逻辑为证明指针程序的安全性提供了可行的途径。本文给出了针逻辑系统在一个出具证明编译器原型系统中的实现,该原型证明系统包括一个验证条件生成器和定理证明器,能够根据指针逻辑的公理和推理规则,自动完成断言的生成和证明;并且,这些代码、断言和证明可以被出具证明的编译器继续翻译到目标语言级。本文利用辅助定理证明工具Coq,机械证明了指针逻辑对于操作语义的可靠性定理。
本文研究了指针逻辑在面向对象语言上的应用。本文设计了一个小的面向对象语言Cool并定义了它的形式语义;Cool保留了Java语言核心的的语法元素,如类、对象、继承等。本文扩展了指针逻辑以增加对这些新语言特性的支持。除了作为通用的程序逻辑外,本文还研究了指针逻辑在静态垃圾判断方面的应用。具体的,本文研究了指针逻辑判断静态垃圾的两种典型应用:栈分配和静态垃圾判断。栈分配可以通过把对象分配到栈而不是堆上,有效的减少垃圾的产生;而静态垃圾判断可以静态判断堆上的垃圾。
本文的研究工作是对基于程序性质证明的安全软件开发框架的初步探索,但本文所研究的以指针逻辑为基础的程序性质证明方法为更大规模和更实际的软件系统安全性证明提供了一条可行的途径。
Nowadays, information technologies play more and more important roles in all aspects of our world: industries, governments, bussiness, and schools. Once a node in this network collapses, an expensice catastrophe would happen. As a result, the requirement for software safety and security becomes more and more urgent. To moderate this disparity, developing high-assurance software based on formal methods is an essential approach. Among various formal methods, language-based approach to software security has attracted widespread attention in the past decade. These approaches help reduce the Trusted Computing Base of software systems by starting from the base of software, that is, programming languages and compilers.
One promising approach for high secure software development in the future is the software property proving-based framework. In this framework, programmers design safety policies and decribe them as software specifications, which are fed to the compilers along with normal program code. In order to prove these programs satisfy these specifications, the compiler generates verification conditions, which are proved automatically or interatively by the programmers. A compiler translates these program code, along with those verification conditions and proofs, and such kind of compilers are called certifying compiler. At the assembly level, an independent proof checker checks the object code to ensure it satisfy its specifications. The key benifit of this framework is that it offers source-level proof methods, instead of at assembly-level, which makes the process of program development more effecient. Meanwhile, making use of a certifing compiler greatly reduces the trusted computing base by removing the compier and prover from the TCB.
As an integral part of the above framework, this thesis investigates pointer logic and its application to source code proving. This thesis designs PointerC, a C-like imperative language which retains C's explicit memory management facilities. The primary design motivation for PointerC is our goal to study more expressive safetye polies beyond type safety such as memory safety. And this thesis makes use of a static discipline combining type system and pointer logic system.
This thesis proposes a novel program logic, i.e., the pointer logic. The primary goal for the design of pointer logic is: on on hand, traditional type system are weak and could not check the value-related safety obligations; on the other hand, Hoare logic can not handle pointer operations directly. The pointer logic extends traditional Hoare logic with new predicates and operations, and presents new deduction rules. The pointer logic has been implemented in our prototype certifying compiler and has been employed to prove some nontrivial pointer programs. This thesis proves pointer logic soundness with respect to operational semantics.
This thesis investigates the application of the pointer logic to a small object-oriented language. To be specific, this thesis designs a small object-oriented language Cool, presents its syntax, static and dynamic semantics. Comparing with the pointer logic for PointerC, the pointer logic for Cool can also serve as a static garbage detection tool, which is capable to detect garbages in two ways: stack-allocation and static detection. Stack-allocation reduces the existence of garbage by allocating objects on stacks, instead of in heaps. And static garbage could detect some static garbages at compile time.
The work presented in this thesis is the first step to the investigation of property proving-based software safety research. And this work provides a method to the safety verifications of larger and more practical saftware systems.
未来高安全软件设计和开发的一种行之有效的方式将是基于程序性质证明的开发框架。在这个框架中,程序设计者将软件的安全策略等描述成程序应满足的规范,连同程序一起提交给编译器:编译器生成为证明程序满足规范所需的验证条件,并且利用内嵌的定理证明器自动地或交互地证明这些验证条件;编译器在把源程序翻译成目标代码的同时,将源程序满足规范的证明翻译成目标代码满足等效规范的证明,这样的编译器称为出具证明的编译器(certifyingcompiler);在目标代码一级由证明检验器利用代码所携带的证明自动进行代码满足规范的检验。该框架的主要优点是,它向程序设计者提供源级而不是目标级的程序性质证明方法,以提高安全程序的开发效率,同时它将编译器、证明器等排除出受信任的计算基础,以尽量缩小系统的TCB。
作为上述基于程序性质证明的软件安全长期研究工作的一个环节和组成部分,本文在指针逻辑以及基于指针逻辑的源代码性质描述和性质证明方面做了有益探索。
本文首先研究了一个强调指针类型的类C的命令式语言源语言PointerC的设计并给出了它的安全性证明。PointerC语言设计的主要出发点是:已有软件安全和出具证明编译的研究大多集中在类型安全等简单安全策略上;而本文研究的高安全程序设计框架关注更实际、更丰富的安全策略,如内存安全等,因此,PointerC保留了C语言指针特性。本文给出了一种易于程序员理解的安全语言描述方式,并尝试以类型系统和逻辑系统相结合的静态机制来推理程序的安全性。本文利用辅助定理证明工具Coq,机械证明了PointerC语言的安全性定理。
本文研究了一种指针逻辑系统。指针逻辑扩展了传统Hoare逻辑,并加入了新的推理规则以支持对指针操作的推理,因此指针逻辑为证明指针程序的安全性提供了可行的途径。本文给出了针逻辑系统在一个出具证明编译器原型系统中的实现,该原型证明系统包括一个验证条件生成器和定理证明器,能够根据指针逻辑的公理和推理规则,自动完成断言的生成和证明;并且,这些代码、断言和证明可以被出具证明的编译器继续翻译到目标语言级。本文利用辅助定理证明工具Coq,机械证明了指针逻辑对于操作语义的可靠性定理。
本文研究了指针逻辑在面向对象语言上的应用。本文设计了一个小的面向对象语言Cool并定义了它的形式语义;Cool保留了Java语言核心的的语法元素,如类、对象、继承等。本文扩展了指针逻辑以增加对这些新语言特性的支持。除了作为通用的程序逻辑外,本文还研究了指针逻辑在静态垃圾判断方面的应用。具体的,本文研究了指针逻辑判断静态垃圾的两种典型应用:栈分配和静态垃圾判断。栈分配可以通过把对象分配到栈而不是堆上,有效的减少垃圾的产生;而静态垃圾判断可以静态判断堆上的垃圾。
本文的研究工作是对基于程序性质证明的安全软件开发框架的初步探索,但本文所研究的以指针逻辑为基础的程序性质证明方法为更大规模和更实际的软件系统安全性证明提供了一条可行的途径。
Nowadays, information technologies play more and more important roles in all aspects of our world: industries, governments, bussiness, and schools. Once a node in this network collapses, an expensice catastrophe would happen. As a result, the requirement for software safety and security becomes more and more urgent. To moderate this disparity, developing high-assurance software based on formal methods is an essential approach. Among various formal methods, language-based approach to software security has attracted widespread attention in the past decade. These approaches help reduce the Trusted Computing Base of software systems by starting from the base of software, that is, programming languages and compilers.
One promising approach for high secure software development in the future is the software property proving-based framework. In this framework, programmers design safety policies and decribe them as software specifications, which are fed to the compilers along with normal program code. In order to prove these programs satisfy these specifications, the compiler generates verification conditions, which are proved automatically or interatively by the programmers. A compiler translates these program code, along with those verification conditions and proofs, and such kind of compilers are called certifying compiler. At the assembly level, an independent proof checker checks the object code to ensure it satisfy its specifications. The key benifit of this framework is that it offers source-level proof methods, instead of at assembly-level, which makes the process of program development more effecient. Meanwhile, making use of a certifing compiler greatly reduces the trusted computing base by removing the compier and prover from the TCB.
As an integral part of the above framework, this thesis investigates pointer logic and its application to source code proving. This thesis designs PointerC, a C-like imperative language which retains C's explicit memory management facilities. The primary design motivation for PointerC is our goal to study more expressive safetye polies beyond type safety such as memory safety. And this thesis makes use of a static discipline combining type system and pointer logic system.
This thesis proposes a novel program logic, i.e., the pointer logic. The primary goal for the design of pointer logic is: on on hand, traditional type system are weak and could not check the value-related safety obligations; on the other hand, Hoare logic can not handle pointer operations directly. The pointer logic extends traditional Hoare logic with new predicates and operations, and presents new deduction rules. The pointer logic has been implemented in our prototype certifying compiler and has been employed to prove some nontrivial pointer programs. This thesis proves pointer logic soundness with respect to operational semantics.
This thesis investigates the application of the pointer logic to a small object-oriented language. To be specific, this thesis designs a small object-oriented language Cool, presents its syntax, static and dynamic semantics. Comparing with the pointer logic for PointerC, the pointer logic for Cool can also serve as a static garbage detection tool, which is capable to detect garbages in two ways: stack-allocation and static detection. Stack-allocation reduces the existence of garbage by allocating objects on stacks, instead of in heaps. And static garbage could detect some static garbages at compile time.
The work presented in this thesis is the first step to the investigation of property proving-based software safety research. And this work provides a method to the safety verifications of larger and more practical saftware systems.
引文
葛琳.2007年.可信软件开发框架下的出具证明编译研究[D].[S.1.]:中国科学技术大学.http://ssg.ustcsz.edu.cn.
APPEL A W.2001.Foundational Proof-Carrying Code[C]//Logic in Computer Science.[S.1.]:[s.n.],citeseer,ist.psu.edu/appe101foundational.html.
APT K.1981.Ten Years of Hoare's Logic:A Survey-Part Ⅰ[J].ACM Transactions on Programming Languages and Systems,3(4):431-483.
BARENDREGT H P.1988.Introduction to Lambda Calculus[C]//Aspen(?)s Workshop on Implementation of Functional Languages,Goteborg.[S.1.]:Programming Methodology Group,University of Goteborg and Chalmers University of Technology,citeseer,ist.psu.edu/barendregt94introduction.html.
BARNETT M,LEINO K R M,SCHULTE W.2004.The Spec# programming system:An overview[C]//In CASSIS 2004,LNCS vol.3362.[S.1.]:Springer.
BARNETT M,CHANG B Y E,DELINE R,et al.2005.Boogie:A Modular Reusable Verifier for Object-Oriented Programs.[C]//.DE BOER F S,BONSANGUE M M,GRAF S,et al.FMCO.[S.1.]:Springer.Lecture Notes in Computer Science,vol.4111,2007-07-16,http://dblp.uni-trier.de/db/conf/fmco/fmco2005.html#BarnettCDJL05.
BERNDL M,LHOTAK O,QIAN F,et al.2003.Points-to analysis using BDDs[C]//PLDI '03:Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation.New York,NY,USA:ACM:103-114.
BERTOT Y,CASTERAN P.2004.Coq'Art:The Calculus of Inductive Constructions [M].[S.1.]:Springer-Verlag.
BLAZY S,DARGAYE Z,LEROY X.2006.Formal Verification of a C Compiler FrontEnd [C]//FM.[S.1.]:[s.n.]:460-475.
BORNAT R.2000.Proving Pointer Programs in Hoare Logic[C]//MPC'00:Proceedings of the 5th International Conference on Mathematics of Program Construction.London,UK:Springer-Verlag:102-126.
BORNAT R,CALCAGNO C,O'HEARN P,et al.2005.Permission accounting in separation logic[J].SIGPLAN Not.,40(1):259-270.
BOYER R S,MOORE J S.1982.The Correctness Problem in Computer Science[M].Orlando,FL,USA:Academic Press,Inc.
BRUCE K B,CARDELLI L,PIERCE B C.1997.Comparing Object Encodings [C]//Wheoretical Aspects of Computer Software.[S.1.]:[s.n.]:415-438.
CHEN C,XI H.2005.Combining programming with theorem proving[C]//ICFP '05:Proceedings of the tenth ACM SIGPLAN international conference on Functional programming.New York,NY,USA:ACM Press:66-77.
CHEN Y,GE L,HUA B,et al.2007a.Design of a certifying compiler supporting proof of program safety[C]//TASE'07:Proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering.[S.1.]:IEEE Computer Society:117-126.
CHEN Y,GE L,HUA B,et al.2007b.A pointer Logic and Certifying Compiler[J]. Frontiers of Computer Science in China (FCS), 1(3):297-312.
Chen Y, Hua B, Ge L, et al. 2008. (In Chinese). A Pointer Logic for Safety Verification of Pointer Programs[J]. Chinese Journal of Computers, 31(3):372-380.
Cherem S, Rugina R. 2007. Uniqueness inference for compile-time object deallocation[C]//ISMM '07: Proceedings of the 6th international symposium on Memory management. New York, NY, USA: ACM:117-128.
Choi J D, Gupta M, Serrano M, et al. 1999. Escape analysis for Java[C]//OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM: 1-19.
CNCERT/CC. 2007. CNCERT/CC 2006 Annual Report[R].[S.l.]: CNCERT/CC. http://www.cert.org.cn/articles/docs/common/2007042923284.shtml.
Colby C, Lee P, Necula G C, et al. 2000a. A certifying compiler for Java[J]. ACM SIGPLAN Notices, 35(5):95-107.
Colby C, Lee P, Necula G C. 2000b. A Proof-Carrying Code Architecture for Java[C]//Computer Aided Verification. [S.l.]: [s.n.] :557-560, citeseer.ist.psu. edu/colby00proofcarrying.html.
Davies R, Pfenning F. 2000. Intersection types and computational effects[CJ//ICFP '00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM Press:198-208.
DeMillo R A, Lipton R J, Perlis A J. 1977. Social processes and proofs of theorems and programs[C]//POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. New York, NY, USA: ACM Press:206-214.
Detlefs D. 1996. An overview of the Extended Static Checking system[J]. citeseer. ist.psu.edu/detlefs95overview.html.
Detlefs D, Nelson G, Saxe J B. 2005. Simplify: a theorem prover for program checking[J]. J. ACM, 52(3):365-473.
Detlefs D L, Leino K R M, Nelson G, et al. 1998. Extended Static Checking[R]. Palo Alto, USA: [s.n.] .
Dukstra E W. 1975. Guarded commands, non-determinacy and a calculus for the derivation of programs[C]//Proceedings of the international conference on Reliable software. [S.l.]: [s.n.] :2-2.13.
Dukstra E W. 1997. A Discipline of Programming[M]. Upper Saddle River, NJ, USA: Prentice Hall PTR.
Drossopoulou S, Eisenbach S, Khurshid S. 1999. Is the Java type system sound?[J], Theor. Pract. Object Syst., 5(1):3-24.
Dunfield J, Pfenning F. 2004. Tridirectional typechecking[C]//POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:281-292.
Feng X, Shao Z. 2005. Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination [C]//Proc. 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP'05). [S.l.]: [s.n.] :254-267.
Feng X, Shao Z, Vaynberg A, et al. 2006. Modular Verification of Assembly Code with Stack-Based Control Abstractions[C]//Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06). New York, NY, USA: ACM Press:to appear.
Filliatre J C, Marche C. 2004. Multi-prover Verification of C Programs[C]//ICFEM. [S.l.]: [s.n.] :15-29.
Flanagan C, Leino K R M, Lillibridge M, et al. 2002. Extended Static Checking for Java[C]//Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'2002). [S.l.]: [s.n.] , 37:234-245.
Floyd R W. 1967. Assigning Meanings to Programs[C]//. Schwartz J T. Mathematical Aspects of Computer Science. Providence, Rhode Island: American Mathematical Society. Proceedings of Symposia in Applied Mathematics, vol. 19.
Freeman T, Pfenning F. 1991. Refinement types for ML[C]//PLDI '91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. New York, NY, USA: ACM Press:268-277.
Good D I, London R L, Bledsoe W W. 1975. An interactive program verification system[C]//Proceedings of the international conference on Reliable software. New York, NY, USA: ACM:482-492.
Gordon M, Milner R, Morris L, et al. 1978. A Metalanguage for interactive proof in LCF[C]//POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. New York, NY, USA: ACM Press: 119-130.
Gosling J, Joy B, Steele G, et al. 2005. The Java Language Specification, Third Edition[M]. Englewood Cliffs, New Jersey: Prentice-Hall.
Hamid N A, Shao Z, Trifonov V, et al. 2003. A Syntactic Approach to Foundational Proof Carrying-Code[J]. Journal of Automated Reasoning (Special issue on Proof-Carrying Code), 31(3-4):191-229.
Hind M. 2001. Pointer analysis: haven't we solved this problem yet?[C]//PASTE '01: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering. New York, NY, USA: ACM:54-61.
Hoare C A R. 1969. An axiomatic basis for computer programming[J]. Communications ACM, 12(10):576-580.
Hua B. 2007. An Imperative Core Calculus for Java[R].[S.l.]: CS Department, University of Science and Technology of China, http://ssg.ustcsz.edu.cn/lss/doc/ index.html.
Hua B, Chen Y, Li Z, et al. 2008. (In Chinese). Design and Proof of a Safe Programming Language PointerC[J]. Chinese Journal of Computers, 31(4):556-564.
Igarashi A, Pierce B, Wadler P. 1999. Featherwieght Java: a minimal core calculus for Java and GJ[C]//OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM: 132-146.
Igarashi S, London R L, Luckham D C. 1973. Automatic program verification I: a logical basis and its implementation.[R]. Stanford, CA, USA: [s.n.] .
Jim T, Morrisett G, Grossman D, et al. 2002. Cyclone: A safe dialect of c[C]//USENIX Annual Technical Conference, Monterey, CA, June 2002. [S.l.]: [s.n.] , citeseer.ist.psu.edu/j im02cyclone.html.
Jones S B, Metayer D L. 1989. Compile-time garbage collection by sharing analy-sis[C]//FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture. New York, NY, USA: ACM:54-74.
KING J C. 1971. Proving Programs to be Correct[J]. IEEE Trans. Comput., 20(11):1331-1336.
King J C, Floyd R W. 1970. An interpretation oriented theorem prover over inte-gers[C]//STOC '70: Proceedings of the second annual ACM symposium on Theory of computing. New York, NY, USA: ACM:169-179.
League C, Trifonov V, Shao Z. 2001. Type-Preserving Compilation of Featherweight Java[C]//Foundations of Object-Oriented Languages (FOOL8). London: [s.n.] , citeseer.ist.psu.edu/article/league02typepreserving.html.
Leavens G T, Leino KRM, Müller P. 2007. Specification and verification challenges for sequential object-oriented programs[J]. Form. Asp. Comput., 19(2):159-189.
Li Z. 2006. A framework of function-based certified assembly programming[R].[S.l.]: CS Department, University of Science and Technology of China. http://ssg.ustcsz. edu.cn/lss/doc/index.html.
LIE D, THEKKATH C A, HOROWITZ M. 2003. Implementing an untrusted operating system on trusted hardware[C]//Proceedings of the nineteenth ACM symposium on Operating systems principles.[S.l.]: ACM Press: 178-192.
Mandelbaum Y, Walker D, Harper R. 2003. An effective theory of type refine-ments[C]//ICFP'03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM Press:213-225.
Mazur N, Ross P, Janssens G, et al. 2001. Practical Aspects for a Working Compile Time Garbage Collection System for Mercury[Cj//Proceedings of the 17th International Conference on Logic Programming. London, UK: Springer-Verlag: 105-119.
Mehta F, NIPKOW T. 2005. Proving pointer programs in higher-order logic[J]. Inf. Comput., 199(l-2):200-227.
MOHNEN M. 1995. Efficient Compile-Time Garbage Collection for Arbitrary Data Structures[C]//PLILPS '95: Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs. London, UK: Springer-Verlag:241-258.
Morrisett G, Walker D, Crary K, et al. 1998a. From System F to Typed Assembly Language[C]//25th Symposium on Principle of Programming Lanugages, ACM. San Diego, CA, USA: [s.n.] :85-97.
Morrisett G, Crary K, Glew N, et al. 1998b. Stack-Based Typed Assembly Language[C]//. Kyoto, Japan: [s.n.] , 1473:28-52.
Morrisett G, Walker D, Crary K, et al. 1999a. From System-F to Typed Assembly Language[J]. ACM Transactions on Programming Languages and Systems, 21(3):527-568.
Morrisett G, Crary K, Glew N, et al. 1999b. TALx86: A Realistic Typed Assembly Language[C]//Second ACMSIGPLAN Workshop on Compiler Support for System Software. Atlanta, GA, USA: [s.n.] :25-35. Published as INRIA research report number 0228, March 1999.
NAUMANN D A. 2001. Predicate transformer semantics of a higher-order imperative language with record subtyping[J]. Science of Computer Programming, 41(1): 1-51. citeseer.ist.psu.edu/naumann98predicate.html.
NECULA G C. 1997. Proof-Carrying Code[C]//Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL '97). Paris: [s.n.] :106-119, citeseer.ist.psu.edu/50371.html.
NECULA G C. 1998. Compiling with proofs[D]. [S.l.]: [s.n.] . Chair-Peter Lee.
NECULA G C, Lee P. 1996. Safe Kernel Extensions Without Run-Time Checking[C]//. USENIX. 2nd Symposium on Operating Systems Design and Implementation (OSDI '96), October 28-31, 1996. Seattle, WA. Berkeley, CA, USA: USENIX.-229-243, citeseer.ist.psu.edu/necula96safe.html.
Necula G C, Lee P. 1998. The Design and Implementation of a Certifying Com-piler[C]//Proceedings of the 1998 ACM SIGPLAN Conference on Prgramming Language Design and Implementation (PLDI). [S.l.]: [s.n.] :333-344.
Necula G C, Lee P. 2000. Proof Generation in the Touchstone Theorem Prover[C]//Conference on Automated Deduction. [S.l.]: [s.n.] :25-44, citeseer. ist.psu.edu/necula00proof.html.
Necula G C, Schneck R R. 2003. Proof-carrying code with untrusted proof rules[J]. M. Okada, B. C. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, editors, Software Security . Theories and Systems, Mext-NSF-JSPS International Symposium (ISSS), 2609:283-298.
Necula G C, McPeak S, Weimer W. 2002. CCured: type-safe retrofitting of legacy code[C]//POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:128-139.
NI Z, Shao Z. 2006. Certified Assembly Programming with Embedded Code Pointers. [C]//Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06). [S.l.]: [s.n.] :320-333.
Parkinson M, Bierman G. 2005. Separation logic and abstraction[J]. SIGPLAN Not., 40(1):247-258.
Pierce B C. 2002. Types and Programming Languages[M].[S.l.]: The MIT Press. Reynolds J C. 2002. Separation Logic: A Logic for Shared Mutable Data Struc-tures[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:55-74.
Shao Z. 1997. An Overview of the FLINT/ML Compiler[C]//Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC'97). Amsterdam, The Netherlands: [s.n.] .
Shao Z, Appel A W. 1995. A Type-based Compiler for Standard ML[C]//Proc. 1995 ACM SIGPLAN Conference on Programming Language Design and Implementation. La Jolla, CA: [s.n.] :116-129.
Steensgaard B. 1996. Points-to analysis in almost linear time[C]//POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:32-41.
Tarditi D, Morrisett G, Cheng P, et al. 1996. TIL: A Type-Directed Optimizing Compiler for ML[C]//. Philadelphia, PA: [s.n.] .181-192.
The Coq Development Team. 2004. [S.l.]: [s.n.] . http://coq.inria.fr.
VON Oheimb D. 2001. Hoare Logic for Java in Isabelle/HOL[J]. Concurrency and Computation: Practice and Experience, 13(13):1173-1214.
Whaley J, Rinard M. 1999. Compositional pointer and escape analysis for Java programs[C]//OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM:187-206.
XI H. 1998. Dependent Types in Practical Programming[D].[S.l.]: Carnegie Mellon University, http: //www. ececs. uc. edu/～hwxi/DML/DML.html.
XI H. 2004. Applied Type System (extended abstract)[C]//post-workshop Proceedings of TYPES 2003.[S.l.]: Springer-Verlag LNCS 3085:394-408.
XI H, Pfenning F. 1998. Eliminating Array Bound Checking through Dependent Types[C]//Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. Montreal: [s.n.] :249-257.
XI H, Pfenning F. 1999. Dependent Types in Practical Programming[C]//Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas. New York, NY: [s.n.] :214-227.
XI H, Chen C, Chen G. 2003. Guarded recursive datatype constructors[C]//POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:224-235.
XI H, Zhu D, Li Y. 2005. Applied Type System with Stateful Views[R].[S.I.]: CS Department, Boston University. http://www.cs.bu.edu/techreports/ 2005-003-ATSwSV.ps.Z.
Yu D, Shao Z. 2004. Verification of Safety Properties for Concurrent Assembly Code[C]//Proc. 2004 International Conference on Functional Programming (ICFP'04). [S.l.]: [s.n.] .
Yu D, Hamid N A, Shao Z. 2003. Building Certified Libraries for PCC: Dynamic Storage Allocation[C]//Proceedings 12th European Symposium on Programming (ESOP 2003).[S.l.]: Springer. LNCS, vol. 2618.
APPEL A W.2001.Foundational Proof-Carrying Code[C]//Logic in Computer Science.[S.1.]:[s.n.],citeseer,ist.psu.edu/appe101foundational.html.
APT K.1981.Ten Years of Hoare's Logic:A Survey-Part Ⅰ[J].ACM Transactions on Programming Languages and Systems,3(4):431-483.
BARENDREGT H P.1988.Introduction to Lambda Calculus[C]//Aspen(?)s Workshop on Implementation of Functional Languages,Goteborg.[S.1.]:Programming Methodology Group,University of Goteborg and Chalmers University of Technology,citeseer,ist.psu.edu/barendregt94introduction.html.
BARNETT M,LEINO K R M,SCHULTE W.2004.The Spec# programming system:An overview[C]//In CASSIS 2004,LNCS vol.3362.[S.1.]:Springer.
BARNETT M,CHANG B Y E,DELINE R,et al.2005.Boogie:A Modular Reusable Verifier for Object-Oriented Programs.[C]//.DE BOER F S,BONSANGUE M M,GRAF S,et al.FMCO.[S.1.]:Springer.Lecture Notes in Computer Science,vol.4111,2007-07-16,http://dblp.uni-trier.de/db/conf/fmco/fmco2005.html#BarnettCDJL05.
BERNDL M,LHOTAK O,QIAN F,et al.2003.Points-to analysis using BDDs[C]//PLDI '03:Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation.New York,NY,USA:ACM:103-114.
BERTOT Y,CASTERAN P.2004.Coq'Art:The Calculus of Inductive Constructions [M].[S.1.]:Springer-Verlag.
BLAZY S,DARGAYE Z,LEROY X.2006.Formal Verification of a C Compiler FrontEnd [C]//FM.[S.1.]:[s.n.]:460-475.
BORNAT R.2000.Proving Pointer Programs in Hoare Logic[C]//MPC'00:Proceedings of the 5th International Conference on Mathematics of Program Construction.London,UK:Springer-Verlag:102-126.
BORNAT R,CALCAGNO C,O'HEARN P,et al.2005.Permission accounting in separation logic[J].SIGPLAN Not.,40(1):259-270.
BOYER R S,MOORE J S.1982.The Correctness Problem in Computer Science[M].Orlando,FL,USA:Academic Press,Inc.
BRUCE K B,CARDELLI L,PIERCE B C.1997.Comparing Object Encodings [C]//Wheoretical Aspects of Computer Software.[S.1.]:[s.n.]:415-438.
CHEN C,XI H.2005.Combining programming with theorem proving[C]//ICFP '05:Proceedings of the tenth ACM SIGPLAN international conference on Functional programming.New York,NY,USA:ACM Press:66-77.
CHEN Y,GE L,HUA B,et al.2007a.Design of a certifying compiler supporting proof of program safety[C]//TASE'07:Proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering.[S.1.]:IEEE Computer Society:117-126.
CHEN Y,GE L,HUA B,et al.2007b.A pointer Logic and Certifying Compiler[J]. Frontiers of Computer Science in China (FCS), 1(3):297-312.
Chen Y, Hua B, Ge L, et al. 2008. (In Chinese). A Pointer Logic for Safety Verification of Pointer Programs[J]. Chinese Journal of Computers, 31(3):372-380.
Cherem S, Rugina R. 2007. Uniqueness inference for compile-time object deallocation[C]//ISMM '07: Proceedings of the 6th international symposium on Memory management. New York, NY, USA: ACM:117-128.
Choi J D, Gupta M, Serrano M, et al. 1999. Escape analysis for Java[C]//OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM: 1-19.
CNCERT/CC. 2007. CNCERT/CC 2006 Annual Report[R].[S.l.]: CNCERT/CC. http://www.cert.org.cn/articles/docs/common/2007042923284.shtml.
Colby C, Lee P, Necula G C, et al. 2000a. A certifying compiler for Java[J]. ACM SIGPLAN Notices, 35(5):95-107.
Colby C, Lee P, Necula G C. 2000b. A Proof-Carrying Code Architecture for Java[C]//Computer Aided Verification. [S.l.]: [s.n.] :557-560, citeseer.ist.psu. edu/colby00proofcarrying.html.
Davies R, Pfenning F. 2000. Intersection types and computational effects[CJ//ICFP '00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM Press:198-208.
DeMillo R A, Lipton R J, Perlis A J. 1977. Social processes and proofs of theorems and programs[C]//POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. New York, NY, USA: ACM Press:206-214.
Detlefs D. 1996. An overview of the Extended Static Checking system[J]. citeseer. ist.psu.edu/detlefs95overview.html.
Detlefs D, Nelson G, Saxe J B. 2005. Simplify: a theorem prover for program checking[J]. J. ACM, 52(3):365-473.
Detlefs D L, Leino K R M, Nelson G, et al. 1998. Extended Static Checking[R]. Palo Alto, USA: [s.n.] .
Dukstra E W. 1975. Guarded commands, non-determinacy and a calculus for the derivation of programs[C]//Proceedings of the international conference on Reliable software. [S.l.]: [s.n.] :2-2.13.
Dukstra E W. 1997. A Discipline of Programming[M]. Upper Saddle River, NJ, USA: Prentice Hall PTR.
Drossopoulou S, Eisenbach S, Khurshid S. 1999. Is the Java type system sound?[J], Theor. Pract. Object Syst., 5(1):3-24.
Dunfield J, Pfenning F. 2004. Tridirectional typechecking[C]//POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:281-292.
Feng X, Shao Z. 2005. Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination [C]//Proc. 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP'05). [S.l.]: [s.n.] :254-267.
Feng X, Shao Z, Vaynberg A, et al. 2006. Modular Verification of Assembly Code with Stack-Based Control Abstractions[C]//Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06). New York, NY, USA: ACM Press:to appear.
Filliatre J C, Marche C. 2004. Multi-prover Verification of C Programs[C]//ICFEM. [S.l.]: [s.n.] :15-29.
Flanagan C, Leino K R M, Lillibridge M, et al. 2002. Extended Static Checking for Java[C]//Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'2002). [S.l.]: [s.n.] , 37:234-245.
Floyd R W. 1967. Assigning Meanings to Programs[C]//. Schwartz J T. Mathematical Aspects of Computer Science. Providence, Rhode Island: American Mathematical Society. Proceedings of Symposia in Applied Mathematics, vol. 19.
Freeman T, Pfenning F. 1991. Refinement types for ML[C]//PLDI '91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. New York, NY, USA: ACM Press:268-277.
Good D I, London R L, Bledsoe W W. 1975. An interactive program verification system[C]//Proceedings of the international conference on Reliable software. New York, NY, USA: ACM:482-492.
Gordon M, Milner R, Morris L, et al. 1978. A Metalanguage for interactive proof in LCF[C]//POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. New York, NY, USA: ACM Press: 119-130.
Gosling J, Joy B, Steele G, et al. 2005. The Java Language Specification, Third Edition[M]. Englewood Cliffs, New Jersey: Prentice-Hall.
Hamid N A, Shao Z, Trifonov V, et al. 2003. A Syntactic Approach to Foundational Proof Carrying-Code[J]. Journal of Automated Reasoning (Special issue on Proof-Carrying Code), 31(3-4):191-229.
Hind M. 2001. Pointer analysis: haven't we solved this problem yet?[C]//PASTE '01: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering. New York, NY, USA: ACM:54-61.
Hoare C A R. 1969. An axiomatic basis for computer programming[J]. Communications ACM, 12(10):576-580.
Hua B. 2007. An Imperative Core Calculus for Java[R].[S.l.]: CS Department, University of Science and Technology of China, http://ssg.ustcsz.edu.cn/lss/doc/ index.html.
Hua B, Chen Y, Li Z, et al. 2008. (In Chinese). Design and Proof of a Safe Programming Language PointerC[J]. Chinese Journal of Computers, 31(4):556-564.
Igarashi A, Pierce B, Wadler P. 1999. Featherwieght Java: a minimal core calculus for Java and GJ[C]//OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM: 132-146.
Igarashi S, London R L, Luckham D C. 1973. Automatic program verification I: a logical basis and its implementation.[R]. Stanford, CA, USA: [s.n.] .
Jim T, Morrisett G, Grossman D, et al. 2002. Cyclone: A safe dialect of c[C]//USENIX Annual Technical Conference, Monterey, CA, June 2002. [S.l.]: [s.n.] , citeseer.ist.psu.edu/j im02cyclone.html.
Jones S B, Metayer D L. 1989. Compile-time garbage collection by sharing analy-sis[C]//FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture. New York, NY, USA: ACM:54-74.
KING J C. 1971. Proving Programs to be Correct[J]. IEEE Trans. Comput., 20(11):1331-1336.
King J C, Floyd R W. 1970. An interpretation oriented theorem prover over inte-gers[C]//STOC '70: Proceedings of the second annual ACM symposium on Theory of computing. New York, NY, USA: ACM:169-179.
League C, Trifonov V, Shao Z. 2001. Type-Preserving Compilation of Featherweight Java[C]//Foundations of Object-Oriented Languages (FOOL8). London: [s.n.] , citeseer.ist.psu.edu/article/league02typepreserving.html.
Leavens G T, Leino KRM, Müller P. 2007. Specification and verification challenges for sequential object-oriented programs[J]. Form. Asp. Comput., 19(2):159-189.
Li Z. 2006. A framework of function-based certified assembly programming[R].[S.l.]: CS Department, University of Science and Technology of China. http://ssg.ustcsz. edu.cn/lss/doc/index.html.
LIE D, THEKKATH C A, HOROWITZ M. 2003. Implementing an untrusted operating system on trusted hardware[C]//Proceedings of the nineteenth ACM symposium on Operating systems principles.[S.l.]: ACM Press: 178-192.
Mandelbaum Y, Walker D, Harper R. 2003. An effective theory of type refine-ments[C]//ICFP'03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM Press:213-225.
Mazur N, Ross P, Janssens G, et al. 2001. Practical Aspects for a Working Compile Time Garbage Collection System for Mercury[Cj//Proceedings of the 17th International Conference on Logic Programming. London, UK: Springer-Verlag: 105-119.
Mehta F, NIPKOW T. 2005. Proving pointer programs in higher-order logic[J]. Inf. Comput., 199(l-2):200-227.
MOHNEN M. 1995. Efficient Compile-Time Garbage Collection for Arbitrary Data Structures[C]//PLILPS '95: Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs. London, UK: Springer-Verlag:241-258.
Morrisett G, Walker D, Crary K, et al. 1998a. From System F to Typed Assembly Language[C]//25th Symposium on Principle of Programming Lanugages, ACM. San Diego, CA, USA: [s.n.] :85-97.
Morrisett G, Crary K, Glew N, et al. 1998b. Stack-Based Typed Assembly Language[C]//. Kyoto, Japan: [s.n.] , 1473:28-52.
Morrisett G, Walker D, Crary K, et al. 1999a. From System-F to Typed Assembly Language[J]. ACM Transactions on Programming Languages and Systems, 21(3):527-568.
Morrisett G, Crary K, Glew N, et al. 1999b. TALx86: A Realistic Typed Assembly Language[C]//Second ACMSIGPLAN Workshop on Compiler Support for System Software. Atlanta, GA, USA: [s.n.] :25-35. Published as INRIA research report number 0228, March 1999.
NAUMANN D A. 2001. Predicate transformer semantics of a higher-order imperative language with record subtyping[J]. Science of Computer Programming, 41(1): 1-51. citeseer.ist.psu.edu/naumann98predicate.html.
NECULA G C. 1997. Proof-Carrying Code[C]//Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL '97). Paris: [s.n.] :106-119, citeseer.ist.psu.edu/50371.html.
NECULA G C. 1998. Compiling with proofs[D]. [S.l.]: [s.n.] . Chair-Peter Lee.
NECULA G C, Lee P. 1996. Safe Kernel Extensions Without Run-Time Checking[C]//. USENIX. 2nd Symposium on Operating Systems Design and Implementation (OSDI '96), October 28-31, 1996. Seattle, WA. Berkeley, CA, USA: USENIX.-229-243, citeseer.ist.psu.edu/necula96safe.html.
Necula G C, Lee P. 1998. The Design and Implementation of a Certifying Com-piler[C]//Proceedings of the 1998 ACM SIGPLAN Conference on Prgramming Language Design and Implementation (PLDI). [S.l.]: [s.n.] :333-344.
Necula G C, Lee P. 2000. Proof Generation in the Touchstone Theorem Prover[C]//Conference on Automated Deduction. [S.l.]: [s.n.] :25-44, citeseer. ist.psu.edu/necula00proof.html.
Necula G C, Schneck R R. 2003. Proof-carrying code with untrusted proof rules[J]. M. Okada, B. C. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, editors, Software Security . Theories and Systems, Mext-NSF-JSPS International Symposium (ISSS), 2609:283-298.
Necula G C, McPeak S, Weimer W. 2002. CCured: type-safe retrofitting of legacy code[C]//POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:128-139.
NI Z, Shao Z. 2006. Certified Assembly Programming with Embedded Code Pointers. [C]//Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06). [S.l.]: [s.n.] :320-333.
Parkinson M, Bierman G. 2005. Separation logic and abstraction[J]. SIGPLAN Not., 40(1):247-258.
Pierce B C. 2002. Types and Programming Languages[M].[S.l.]: The MIT Press. Reynolds J C. 2002. Separation Logic: A Logic for Shared Mutable Data Struc-tures[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:55-74.
Shao Z. 1997. An Overview of the FLINT/ML Compiler[C]//Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC'97). Amsterdam, The Netherlands: [s.n.] .
Shao Z, Appel A W. 1995. A Type-based Compiler for Standard ML[C]//Proc. 1995 ACM SIGPLAN Conference on Programming Language Design and Implementation. La Jolla, CA: [s.n.] :116-129.
Steensgaard B. 1996. Points-to analysis in almost linear time[C]//POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:32-41.
Tarditi D, Morrisett G, Cheng P, et al. 1996. TIL: A Type-Directed Optimizing Compiler for ML[C]//. Philadelphia, PA: [s.n.] .181-192.
The Coq Development Team. 2004. [S.l.]: [s.n.] . http://coq.inria.fr.
VON Oheimb D. 2001. Hoare Logic for Java in Isabelle/HOL[J]. Concurrency and Computation: Practice and Experience, 13(13):1173-1214.
Whaley J, Rinard M. 1999. Compositional pointer and escape analysis for Java programs[C]//OOPSLA '99: Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. New York, NY, USA: ACM:187-206.
XI H. 1998. Dependent Types in Practical Programming[D].[S.l.]: Carnegie Mellon University, http: //www. ececs. uc. edu/～hwxi/DML/DML.html.
XI H. 2004. Applied Type System (extended abstract)[C]//post-workshop Proceedings of TYPES 2003.[S.l.]: Springer-Verlag LNCS 3085:394-408.
XI H, Pfenning F. 1998. Eliminating Array Bound Checking through Dependent Types[C]//Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation. Montreal: [s.n.] :249-257.
XI H, Pfenning F. 1999. Dependent Types in Practical Programming[C]//Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas. New York, NY: [s.n.] :214-227.
XI H, Chen C, Chen G. 2003. Guarded recursive datatype constructors[C]//POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:224-235.
XI H, Zhu D, Li Y. 2005. Applied Type System with Stateful Views[R].[S.I.]: CS Department, Boston University. http://www.cs.bu.edu/techreports/ 2005-003-ATSwSV.ps.Z.
Yu D, Shao Z. 2004. Verification of Safety Properties for Concurrent Assembly Code[C]//Proc. 2004 International Conference on Functional Programming (ICFP'04). [S.l.]: [s.n.] .
Yu D, Hamid N A, Shao Z. 2003. Building Certified Libraries for PCC: Dynamic Storage Allocation[C]//Proceedings 12th European Symposium on Programming (ESOP 2003).[S.l.]: Springer. LNCS, vol. 2618.