汇编指针程序安全性验证的研究
|
摘要
随着计算机科学的飞速发展和计算机在全球日益普及,计算机软件越来越广泛的应用于各个行业。国家和社会的关键领域对软件的依赖程度日益增长,使得关键软件的高可信性质显得越来越重要,其中安全性是关注的重点。提高软件安全性的目标是:所有的程序错误在程序运行前被发现或者在程序运行时被温和地捕获,以保证程序不会导致不可预测的系统行为。而软件安全性研究主要是探索如何建立一个管理安全性的健全的科学和技术基础,其中软件满足安全策略的程序性质证明方法是研究的热点之一。
近十年来,程序性质证明研究领域有了很大的发展。许多学者提出了不同的思路,这些思路主要采用基于类型的或基于逻辑的方法,来证明高级语言程序或低级语言程序的性质。程序性质证明采用类型方法和逻辑方法相结合方式可以兼得两种方法的长处。因此,本文作者所在的项目组(以下简称本项目组)选择采用一个简单的类型系统结合一个自动的逻辑推理系统的方法来证明程序满足安全策略。对那些有高安全要求的关键软件,程序设计及安全性证明可以在一种新的编程和编译框架下进行。在这个框架下,本项目组选择类C语言PointerC(带有动态存储分配)作为源语言,实现了一个出具证明编译器的原型;并且实现了类型安全和内存安全等基本安全策略。该出具证明的编译器在把源程序和规范翻译成汇编程序和等效规范的同时,将源程序满足规范的证明翻译成汇编代码满足等效规范的证明。在汇编语言一级由证明检查器利用代码所携带的证明进行代码满足规范的检验。汇编语言上的验证可以将编译器、验证条件生成器、定理证明器等排除出TCB,以尽量缩小系统的TCB。因而整个编译框架最终依赖于汇编程序形式验证框架,来保证产生的汇编程序满足汇编语言一级等效的安全规范。
本文介绍作者在汇编级程序验证框架方面的研究。而在众多计算机程序中,指针程序的安全性质最为复杂,因此汇编指针程序安全性质的验证是本文的重点。本文的工作主要基于Hoare逻辑、携带证明代码(Proof-Carrying Code)和验证汇编编程(Certified Assembly Programming)等研究,采用类型和逻辑相结合的研究方法。
本文首先介绍了基于程序性质证明的软件安全的相关研究和指针程序性质证明等方面的研究,然后介绍了本项目组提出的一个使用指针逻辑的安全软件丌发和验证框架。基于该框架下,本文着重介绍汇编程序一级的验证框架的设计和实现。本文提出了汇编级指针逻辑来对汇编指针程序安全性质的进行验证。本文还实现了一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证。
本文的主要特色和贡献为:
●设计了一种基于x86机器模型、Hoare逻辑风格的形式证明框架,丰富了出具证明编译器的目标级基础研究。
●设计了一种用于汇编指针程序安全性证明的指针逻辑,解决了Hoare逻辑处理别名面临的困难,使得拓展后的指针逻辑成为汇编程序性质证明的一种新工具。
●证明了汇编语言指针逻辑的可靠性。并已在证明辅助工具Coq中完成。
●实现了一个汇编级验证原型系统。本文使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证。
本工作的意义在于给出一种汇编指针程序验证的新思路,并设计实现了一个可用的原型系统,丰富了程序性质证明的研究和应用。
With the rapid development of computer science and technology,computer software is more and more widely used in various industries.The dependence of computer software using in the key areas of the state and society is growing.So high-assurance software is more and more valued,and among its properties,safety and security are most important.The objective to improve software safety is:all program errors in the programs were discovered before the program is executed,or were captured moderately.Thus it ensures that programs would not result in unpredictable system behaviors.The research goal of software safety is to build a wholesome scientific and technological infrastructure for the management of software safety.And the verification method for software to meet its safety policies is one of the hot researches.
In the past decade,great progress has been made in the area of program verification.Proof-Carrying Code brings two grand challenges to the research field of programming languages.By analysis of the current research situation,combining both type-based and logic-based approaches is a better way.We have designed a high-assurance software development infrastructure.In this infrastructure programs are certified to meet their safety policies using a simple type system and a logic system.In this infrastructure,source-level and assembly-level program verification could be done simultaneously,and a certifying compiler produces assembly-level safety proofs automatically from the source-level specifications and safety proofs.
In terms of our infrastructure to design and verification of safety programs,and the pointer logic proof system,this dissertation presents the research work in assembly-level program verification.Among various computer programs,the programs containing pointers are more complex to reason about.So the research on verification of assembly pointer programs is an emphasis.The work in this dissertation is inspired by Hoare Logic,PCC(Proof-Carrying Code)and CAP (Certified Assembly Programming)etc.,and adopts an approach of combining both types and logics.
This dissertation firstly introduces our research background on software safety and verification of pointer programs.Then a high-assurance software development infrastructure is presented.Under this infrastructure,the design and implementation of the assembly verification framework will be introduced.
The main characteristics and contributions of this dissertation are:
●A design of formal verification framework(Function-based Certifying Assembly Programming,FCAP)based on a x86 target machine.It is based on Intel x86 target machine.
●A design of the assembly pointer logic(APL)for reasoning the safety of the assembly pointer programs.It has resolved difficulties to deal with the aliases using Hoare logic.It assures that there will be no null-pointer dereferences and no memory leak after the program is passed the verification.
●Proof of the soundness of the assembly pointer logic is finished in the proof assistant Coq.
●Implementation of a prototype system of the assembly-level verification framework.And using this prototype system,some non-trivial pointer programs of operations on the lists and binary trees have been verified.
This dissertation was supported by Chinese Natural Science Foundation under Grant No.60673126 and Intel China Research Center(Beijing).
近十年来,程序性质证明研究领域有了很大的发展。许多学者提出了不同的思路,这些思路主要采用基于类型的或基于逻辑的方法,来证明高级语言程序或低级语言程序的性质。程序性质证明采用类型方法和逻辑方法相结合方式可以兼得两种方法的长处。因此,本文作者所在的项目组(以下简称本项目组)选择采用一个简单的类型系统结合一个自动的逻辑推理系统的方法来证明程序满足安全策略。对那些有高安全要求的关键软件,程序设计及安全性证明可以在一种新的编程和编译框架下进行。在这个框架下,本项目组选择类C语言PointerC(带有动态存储分配)作为源语言,实现了一个出具证明编译器的原型;并且实现了类型安全和内存安全等基本安全策略。该出具证明的编译器在把源程序和规范翻译成汇编程序和等效规范的同时,将源程序满足规范的证明翻译成汇编代码满足等效规范的证明。在汇编语言一级由证明检查器利用代码所携带的证明进行代码满足规范的检验。汇编语言上的验证可以将编译器、验证条件生成器、定理证明器等排除出TCB,以尽量缩小系统的TCB。因而整个编译框架最终依赖于汇编程序形式验证框架,来保证产生的汇编程序满足汇编语言一级等效的安全规范。
本文介绍作者在汇编级程序验证框架方面的研究。而在众多计算机程序中,指针程序的安全性质最为复杂,因此汇编指针程序安全性质的验证是本文的重点。本文的工作主要基于Hoare逻辑、携带证明代码(Proof-Carrying Code)和验证汇编编程(Certified Assembly Programming)等研究,采用类型和逻辑相结合的研究方法。
本文首先介绍了基于程序性质证明的软件安全的相关研究和指针程序性质证明等方面的研究,然后介绍了本项目组提出的一个使用指针逻辑的安全软件丌发和验证框架。基于该框架下,本文着重介绍汇编程序一级的验证框架的设计和实现。本文提出了汇编级指针逻辑来对汇编指针程序安全性质的进行验证。本文还实现了一个原型系统,并使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证。
本文的主要特色和贡献为:
●设计了一种基于x86机器模型、Hoare逻辑风格的形式证明框架,丰富了出具证明编译器的目标级基础研究。
●设计了一种用于汇编指针程序安全性证明的指针逻辑,解决了Hoare逻辑处理别名面临的困难,使得拓展后的指针逻辑成为汇编程序性质证明的一种新工具。
●证明了汇编语言指针逻辑的可靠性。并已在证明辅助工具Coq中完成。
●实现了一个汇编级验证原型系统。本文使用该系统对链表、二叉树等非平凡的指针程序的进行了自动的安全验证。
本工作的意义在于给出一种汇编指针程序验证的新思路,并设计实现了一个可用的原型系统,丰富了程序性质证明的研究和应用。
With the rapid development of computer science and technology,computer software is more and more widely used in various industries.The dependence of computer software using in the key areas of the state and society is growing.So high-assurance software is more and more valued,and among its properties,safety and security are most important.The objective to improve software safety is:all program errors in the programs were discovered before the program is executed,or were captured moderately.Thus it ensures that programs would not result in unpredictable system behaviors.The research goal of software safety is to build a wholesome scientific and technological infrastructure for the management of software safety.And the verification method for software to meet its safety policies is one of the hot researches.
In the past decade,great progress has been made in the area of program verification.Proof-Carrying Code brings two grand challenges to the research field of programming languages.By analysis of the current research situation,combining both type-based and logic-based approaches is a better way.We have designed a high-assurance software development infrastructure.In this infrastructure programs are certified to meet their safety policies using a simple type system and a logic system.In this infrastructure,source-level and assembly-level program verification could be done simultaneously,and a certifying compiler produces assembly-level safety proofs automatically from the source-level specifications and safety proofs.
In terms of our infrastructure to design and verification of safety programs,and the pointer logic proof system,this dissertation presents the research work in assembly-level program verification.Among various computer programs,the programs containing pointers are more complex to reason about.So the research on verification of assembly pointer programs is an emphasis.The work in this dissertation is inspired by Hoare Logic,PCC(Proof-Carrying Code)and CAP (Certified Assembly Programming)etc.,and adopts an approach of combining both types and logics.
This dissertation firstly introduces our research background on software safety and verification of pointer programs.Then a high-assurance software development infrastructure is presented.Under this infrastructure,the design and implementation of the assembly verification framework will be introduced.
The main characteristics and contributions of this dissertation are:
●A design of formal verification framework(Function-based Certifying Assembly Programming,FCAP)based on a x86 target machine.It is based on Intel x86 target machine.
●A design of the assembly pointer logic(APL)for reasoning the safety of the assembly pointer programs.It has resolved difficulties to deal with the aliases using Hoare logic.It assures that there will be no null-pointer dereferences and no memory leak after the program is passed the verification.
●Proof of the soundness of the assembly pointer logic is finished in the proof assistant Coq.
●Implementation of a prototype system of the assembly-level verification framework.And using this prototype system,some non-trivial pointer programs of operations on the lists and binary trees have been verified.
This dissertation was supported by Chinese Natural Science Foundation under Grant No.60673126 and Intel China Research Center(Beijing).
引文
陈火旺,王戟.计算机科学技术面临的挑战-高可信软什技术[EB/OL].[2008-4-20].http://dragonstar.ict.ac.cn/workshop/ws002.ppt.
陈意云,华保健,葛琳等,2008年,一种用于指针程序安全性证明的指针逻辑[J].计算机学报,31(3):372-380.
葛琳,2007年,可信软件开发框架下的出具证明编译研究[D].Ph.D.thesis,中国科学技术大学.
葛琳,陈意云,华保健等,2008年,汇编代码验证中的形式规范自动生成[J].小型微型计算机系统,已录用.
华保健,陈意云,李兆鹏等,2008年,安全语言PointerC的设计与形式证明[J].计算机学报,31(4):556-564。
华保健,陈意云,李兆鹏等,2007年,一种安全语言的设计与形式证明[C].2007年中国计算机大会文集(CNCC2007),中国计算机学会,清华大学出版社出版。
Appel A.W.,2001,Foundational proof-carrying code[C],In Proc.16th Annual IEEE Symposium on Logic in Computer Science,pages 247-258.
Appel A.W.and McAIlester D.,2001,An indexed model of recursive types for foundational proof-carrying code[J].ACM Trans.Program.Lang.Syst.,vol.23,no.5,pp.657-683.
Apt,K.,1981,Ten years ofhoare's logic:A sur.vey-part I[J].ACM Transactions on Programming Languages and Systems 3(4),431-483.
Barendregt H.P.,1988,Introduction to lambda calculus[C].In Aspenas Workshop on Implementation of Functional Languages,G(?)oteborg,Programming Methodology Group,University of G(?)oteborg and Chalmers University of Technology.
Bornat R.,2000,Proving pointer programs in Hoare logic[C].In Proceedings of the 5th International Conference on Mathematics of Program Construction,pages 102-126,03-05.
Bozga M.,Iosif R.,and Laknech Y.,2003,Storeless semantics and alias logic[C].In Proceedings of PEPM'03,pages 55-65,ACM Press.
Burstall R.M.,1972,Some techniques for proving correctness of programs which alter data structures[J].In B.Meltzer and D.Michie,editors,Machine Intelligence 7,pages 23-50. Edinburgh University Press, Edinburgh, Scotland.
Chen C. and Xi H., 2005, Combining programming with theorem proving[C]. In ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, (New York, NY, USA), pp. 66-77, ACM Press.
Chen Y., Ge L, Hua B., Li Z., Liu C., 2007, Design of a Certifying Compiler Supporting Proof of Program Safety[C]. In proceedings of 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007). pages 117-126, Shanghai, China. IEEE Computer Society.
Chen Y, Ge L, Hua B., Li Z., Liu C, Wang Z.,2007, A Pointer Logic and Certifying CompiIer[J]. Frontiers of Computer Science in China, 1(3), pp. 297-312.
Chen, Y., B. Hua, L. Ge, and Z. Wang. 2008. (In Chinese), A pointer logic for safety verification of pointer programs[J]. Chinese Journal of Computers 31(3), 372.
Clarke E. M., Jr., Grumberg O. and Peled D. A., 1999. Model Checking[M]. MIT Press, ISBN 0-262-03270-8.
Colby C., Lee P., Necula G. C., Blau F., Plesko M., and Cline K., A certifying compiler for Java[J]. ACM SIGPLAN Notices, vol. 35, no. 5, pp. 95-107, 2000.
Colby C., Lee P., and Necula G. C., 2000, A proof-carrying code architecture for java [C]. In Computer Aided Verification, pp. 557-560.
DeLine R. and Fahndrich M., 2001, Enforcing high-level protocols in low-level software[C]. In Proceedings of the ACM Conference on Programming Language Design and Implementation, pages 59-69.
Feng X. and Shao Z., 2005, Modular verification of concurrent assembly code with dynamic thread creation and termination[C]. in Proc. 2005 ACM SIGPLAN International Conference on Functional Progr amming (ICFP'05), pp. 254-267.
Feng X., Shao Z., Vaynberg A., Xiang S., and Ni Z., 2006, Modular verification of assembly code with stack-based control abstractions[C]. In Proc.2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), (New York, NY, USA) , ACM Press.
Feng X., Ni Z., Shao Z., and Guo Y, 2007, An open framework for foundational proof-carrying code[C]. In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07),(New York, NY, USA), pp. 67-78, ACM Press.
Feng X. and Shao Z. and Dong Y. and Guo Y., 2008, Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads[C].2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), ACM Press.
Filliatre J. C. and Marche C, 2004, Multi-prover verification of C programs. In Sixth International Conference on Formal Engineering Methods, LNCS3308, pages 15-29.
Floyd R. W.,1967, Assigning meanings to programs[C], in Mathematical As-pects of Computer Science (J. T. Schwartz, ed.), vol. 19 of Proceedings of Symposia in Applied Mathematics, (Providence, Rhode Island), pp. 19-32, American Mathematical Society.
Hamid N. A., and Shao Z., 2004, Interfacing Hoare logic and type systems for foundational proof-carrying code [C]. In Proc. 17th International Conference on Theorem Proving in Higher Order Logics, volume 3223 of LNCS. pages 118.-135. Springer-Verlag.
Hamid N. A., 2005, A Syntactic Approach to Foundational Proof-Carrying Code[D]. PhD thesis, Yale University.
Harper R. and Pfenning F., 2001, Type refinements[R], project proposal, NSF Grant CCR-0204248.
Hind, M., 2001, Pointer analysis: haven't we solved this problem yet?[C]. In PASTE '01: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering (ACM, New York, NY, USA), pp. 54-61, ISBN 1-58113-413-4.
Hoare C. A. R.,1969, An axiomatic basis for computer programming[J].Communications ACM, vol. 12, no. 10, pp. 576-580.
Howard W.,1980, The formulas-as-types notion of construction[M]. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism (J. P. Seldin and J. R. Hindley, eds.), pp. 479-490, New York, NY Academic Press.
Hua B. J. and Ge L., 2006, The definition of PointerC programming language[EB/OL]. http://ssg.ustcsz.edu.cn/lss/doc/.
Igarashi, S., London R. L., and Luckham D. C., 1973, Automatic program verification i: a logicalbasis and its implementation[R].Automatic program verification I: a logical basis and its implementation., Technical Report, Stanford, CA, USA.
Jackson D., Thomas M., and Millett L. I., Editors, Committee on Certifiably Dependable Software Systems, National Research Council, 2007, Software for Dependable Systems: Sufficient Evidence? [M], The National Academies Press, ISBN: 0-309-66738-0.
Jonkers H. B. M, 1981, Abstract storage structures. In De Bakker and Van Vliet, editors, Algorithmic languages, pages 321-343, IFIP, North Holland.
King, J. C., 1971, Proving programs to be correct[J]. IEEE Trans. Comput. 20(11), 1331, ISSN 0018-9340.
Li, Z., 2006, A framework of function-based certified assembly programming[EB/OL]. A framework of function-based certified assembly programming, Technical Report, CS Department, University of Science and Technology of China. URL http://ssg.ustcsz.edu.cn/lss/doc/index.html.
Li Z., 2006, An implementation of FCAP using the Coq proof assistant[EB/OL]. At http://zero.ustcsz.edu.cn/svn/proiectzero/FCAP/.
Li Z., Wang W, Tian B, 2006, A Proof of Soundness of Assembly Pointer Logic implemented using the Coq proof assistant[EB/OL]. At http://zero.ustcsz.edu.cn/svn/projectzero/.
Mandelbaum, Y., D. Walker, and R. Harper, 2003, An effective theory of type refinements[C]. In ICFP'03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (ACM Press, New York, NY, USA), pp. 213-225,ISBN 1-58113-756-7.
Mehta F. and Nipkow T., 2005, Proving pointer programs in higher-order logic. Information and Computation, 199(1-2), pages 200-227.
Morrisett G., Crary K., Glew N., and Walker D.,1998, Stack-based typed assembly language [C], vol. 1473, (Kyoto, Japan), pp. 28-52.
Morrisett G., Walker D., Crary K. et al, 1998, From system F to typed assembly language [C]. In 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85-97.
Necula G. C. and Lee P, 1996, Proof-Carrying Code[R]. Technical Report CMU-CS-96-165, November.
Necula G. C.,1997, Proof-carrying code[C]. In POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (New York, NY, USA), pp. 106-119, ACM Press.
Necula G. C.,1998, Compiling with Proofs [D]. PhD thesis, School of Computer Science, Carnegie Mellon Univ. N
Necula G. C. and Lee P., 1998, Safe, Untrusted Agents Using Proof-Carrying Code[J]. Mobile Agents and Security, Giovanni Vigna (Ed.), Lecture Notes in Computer Science, Vol. 1419, Springer-Verlag, Berlin, ISBN 3-540-64792-9.
Necula G. C. and Lee P., 1998, The design and implementation of a certifying compiler[C]. In Proceedings of the 1998 ACM SIGPLAN Conference on Prgramming Language Design and Implementation (PLDI), pp. 333-344.
Ni Z. and Shao Z., 2006, Certified assembly programming with embedded code pointers, in Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06), pp. 320-333.
Oheimb D. V., 2001, Hoare logic for Java in Isabelle/HOL [J]. Concurrency and Computation: Practice and Experience, vol. 13, no. 13, pp. 1173-1214.
Parkinson, M., and Bierman G., 2005. Separation logic and abstraction[C]. SIGPLAN Not.40(1), 247, ISSN 0362-1340.
Paulin-Mohring C., 1993, Inductive definitions in the system Coq: Rules and properties[C]. In Proceedings 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93, Utrecht, The Netherlands, 16-18 March 1993 (M. Bezem and J. F. Groote, eds.), vol. 664, pp. 328-345, Berlin:Springer- Verlag.
Pierce, B. C., 2002, Types and Programming Languages[M]. ISBN 0-262-16209-1,The MIT Press.
Reynolds J. C., 2002, Separation logic: a logic for shared mutable data structures[C]. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74, July.
Reynolds J. C.,2005, An introduction to separation logic. Lecture notes[EB/OL], Available at http://www.cs.cmu.edu/jcr/, Spring.
Rometzky M., Bauer J., Reps T, Sagiv M., Wilhelm and R., 2005, A semantics for procedure local heaps and its abstractions[C]. In Proceedings of the 32th Annual ACM Symposium on Principles of Programming Languages, pages 296-309.
Shao Z, 1997, An overview of the FLINT/ML compiler[C], in Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC'97), (Amsterdam,The Netherlands).
Smith F., Walker D., and Morrisett G., 2000, Alias types[C]. In Proceedings of the 2000 European Symposium on Programming, pages 366-381, Berlin.
The Coq Development Team, 2004, The Coq Proof Assistant Reference Manual- Version V8.0[EB/OL], URL http://coq.inria.fr.
Venet A., 1999, Automatic analysis of pointer aliasing for untyped programs[J]. Science of Computer Programming, 35(2):223-248.
Wright A. K. and Felleisen M., 1994, A syntactic approach to type soundness[J]. Information and Computation, 115(1):38—94.
Xi H. ,1998, Dependent Types in Practical Programming[D]. PhD thesis, Carnegie Mellon University.
Xi H. and Pfenning F., 1999, Dependent types in practical programming[C]. I n Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio,Texas, (New York, NY), pp. 214-227.
Xi H., 2000, Imperative programming with dependent types[C]. In Proceedings of 15th IEEE Symposium on Logic in Computer Science, (Santa Barbara), pp. 375-387.
Xi H, Chen C., and Chen G., 2003., Guarded recursive datatype constructors[C]. In POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (New York, NY, USA), pp. 224-235, ACM Press.
Xi H., 2003. Applied type system (extended abstract) [C]. In the post-workshop proceedings of TYPES 2003, volume 3085 of LNCS, pages 394-408. Springer-Verlag.
Xi H., Zhu D., and Li Y, 2005, Applied Type System with Stateful Views[R], Tech. Rep. BUCS-TR-2005-003, CS Department, Boston University.
Yu D., Hamid N. A., and Shao Z., 2003, Building certified libraries for PCC: Dynamic storage allocation[C]. In Proceedings 12th European Symposium on Programming (ESOP 2003), vol. 2618 of LNCS, pp. 363-379, Springer.
Yu D. and Shao Z., 2004, Verification of safety properties for concurrent assembly code[C]. In Proc. 2004 International Conference on Functional Programming (ICFP'04).
陈意云,华保健,葛琳等,2008年,一种用于指针程序安全性证明的指针逻辑[J].计算机学报,31(3):372-380.
葛琳,2007年,可信软件开发框架下的出具证明编译研究[D].Ph.D.thesis,中国科学技术大学.
葛琳,陈意云,华保健等,2008年,汇编代码验证中的形式规范自动生成[J].小型微型计算机系统,已录用.
华保健,陈意云,李兆鹏等,2008年,安全语言PointerC的设计与形式证明[J].计算机学报,31(4):556-564。
华保健,陈意云,李兆鹏等,2007年,一种安全语言的设计与形式证明[C].2007年中国计算机大会文集(CNCC2007),中国计算机学会,清华大学出版社出版。
Appel A.W.,2001,Foundational proof-carrying code[C],In Proc.16th Annual IEEE Symposium on Logic in Computer Science,pages 247-258.
Appel A.W.and McAIlester D.,2001,An indexed model of recursive types for foundational proof-carrying code[J].ACM Trans.Program.Lang.Syst.,vol.23,no.5,pp.657-683.
Apt,K.,1981,Ten years ofhoare's logic:A sur.vey-part I[J].ACM Transactions on Programming Languages and Systems 3(4),431-483.
Barendregt H.P.,1988,Introduction to lambda calculus[C].In Aspenas Workshop on Implementation of Functional Languages,G(?)oteborg,Programming Methodology Group,University of G(?)oteborg and Chalmers University of Technology.
Bornat R.,2000,Proving pointer programs in Hoare logic[C].In Proceedings of the 5th International Conference on Mathematics of Program Construction,pages 102-126,03-05.
Bozga M.,Iosif R.,and Laknech Y.,2003,Storeless semantics and alias logic[C].In Proceedings of PEPM'03,pages 55-65,ACM Press.
Burstall R.M.,1972,Some techniques for proving correctness of programs which alter data structures[J].In B.Meltzer and D.Michie,editors,Machine Intelligence 7,pages 23-50. Edinburgh University Press, Edinburgh, Scotland.
Chen C. and Xi H., 2005, Combining programming with theorem proving[C]. In ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, (New York, NY, USA), pp. 66-77, ACM Press.
Chen Y., Ge L, Hua B., Li Z., Liu C., 2007, Design of a Certifying Compiler Supporting Proof of Program Safety[C]. In proceedings of 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE 2007). pages 117-126, Shanghai, China. IEEE Computer Society.
Chen Y, Ge L, Hua B., Li Z., Liu C, Wang Z.,2007, A Pointer Logic and Certifying CompiIer[J]. Frontiers of Computer Science in China, 1(3), pp. 297-312.
Chen, Y., B. Hua, L. Ge, and Z. Wang. 2008. (In Chinese), A pointer logic for safety verification of pointer programs[J]. Chinese Journal of Computers 31(3), 372.
Clarke E. M., Jr., Grumberg O. and Peled D. A., 1999. Model Checking[M]. MIT Press, ISBN 0-262-03270-8.
Colby C., Lee P., Necula G. C., Blau F., Plesko M., and Cline K., A certifying compiler for Java[J]. ACM SIGPLAN Notices, vol. 35, no. 5, pp. 95-107, 2000.
Colby C., Lee P., and Necula G. C., 2000, A proof-carrying code architecture for java [C]. In Computer Aided Verification, pp. 557-560.
DeLine R. and Fahndrich M., 2001, Enforcing high-level protocols in low-level software[C]. In Proceedings of the ACM Conference on Programming Language Design and Implementation, pages 59-69.
Feng X. and Shao Z., 2005, Modular verification of concurrent assembly code with dynamic thread creation and termination[C]. in Proc. 2005 ACM SIGPLAN International Conference on Functional Progr amming (ICFP'05), pp. 254-267.
Feng X., Shao Z., Vaynberg A., Xiang S., and Ni Z., 2006, Modular verification of assembly code with stack-based control abstractions[C]. In Proc.2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), (New York, NY, USA) , ACM Press.
Feng X., Ni Z., Shao Z., and Guo Y, 2007, An open framework for foundational proof-carrying code[C]. In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07),(New York, NY, USA), pp. 67-78, ACM Press.
Feng X. and Shao Z. and Dong Y. and Guo Y., 2008, Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads[C].2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), ACM Press.
Filliatre J. C. and Marche C, 2004, Multi-prover verification of C programs. In Sixth International Conference on Formal Engineering Methods, LNCS3308, pages 15-29.
Floyd R. W.,1967, Assigning meanings to programs[C], in Mathematical As-pects of Computer Science (J. T. Schwartz, ed.), vol. 19 of Proceedings of Symposia in Applied Mathematics, (Providence, Rhode Island), pp. 19-32, American Mathematical Society.
Hamid N. A., and Shao Z., 2004, Interfacing Hoare logic and type systems for foundational proof-carrying code [C]. In Proc. 17th International Conference on Theorem Proving in Higher Order Logics, volume 3223 of LNCS. pages 118.-135. Springer-Verlag.
Hamid N. A., 2005, A Syntactic Approach to Foundational Proof-Carrying Code[D]. PhD thesis, Yale University.
Harper R. and Pfenning F., 2001, Type refinements[R], project proposal, NSF Grant CCR-0204248.
Hind, M., 2001, Pointer analysis: haven't we solved this problem yet?[C]. In PASTE '01: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering (ACM, New York, NY, USA), pp. 54-61, ISBN 1-58113-413-4.
Hoare C. A. R.,1969, An axiomatic basis for computer programming[J].Communications ACM, vol. 12, no. 10, pp. 576-580.
Howard W.,1980, The formulas-as-types notion of construction[M]. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism (J. P. Seldin and J. R. Hindley, eds.), pp. 479-490, New York, NY Academic Press.
Hua B. J. and Ge L., 2006, The definition of PointerC programming language[EB/OL]. http://ssg.ustcsz.edu.cn/lss/doc/.
Igarashi, S., London R. L., and Luckham D. C., 1973, Automatic program verification i: a logicalbasis and its implementation[R].Automatic program verification I: a logical basis and its implementation., Technical Report, Stanford, CA, USA.
Jackson D., Thomas M., and Millett L. I., Editors, Committee on Certifiably Dependable Software Systems, National Research Council, 2007, Software for Dependable Systems: Sufficient Evidence? [M], The National Academies Press, ISBN: 0-309-66738-0.
Jonkers H. B. M, 1981, Abstract storage structures. In De Bakker and Van Vliet, editors, Algorithmic languages, pages 321-343, IFIP, North Holland.
King, J. C., 1971, Proving programs to be correct[J]. IEEE Trans. Comput. 20(11), 1331, ISSN 0018-9340.
Li, Z., 2006, A framework of function-based certified assembly programming[EB/OL]. A framework of function-based certified assembly programming, Technical Report, CS Department, University of Science and Technology of China. URL http://ssg.ustcsz.edu.cn/lss/doc/index.html.
Li Z., 2006, An implementation of FCAP using the Coq proof assistant[EB/OL]. At http://zero.ustcsz.edu.cn/svn/proiectzero/FCAP/.
Li Z., Wang W, Tian B, 2006, A Proof of Soundness of Assembly Pointer Logic implemented using the Coq proof assistant[EB/OL]. At http://zero.ustcsz.edu.cn/svn/projectzero/.
Mandelbaum, Y., D. Walker, and R. Harper, 2003, An effective theory of type refinements[C]. In ICFP'03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (ACM Press, New York, NY, USA), pp. 213-225,ISBN 1-58113-756-7.
Mehta F. and Nipkow T., 2005, Proving pointer programs in higher-order logic. Information and Computation, 199(1-2), pages 200-227.
Morrisett G., Crary K., Glew N., and Walker D.,1998, Stack-based typed assembly language [C], vol. 1473, (Kyoto, Japan), pp. 28-52.
Morrisett G., Walker D., Crary K. et al, 1998, From system F to typed assembly language [C]. In 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85-97.
Necula G. C. and Lee P, 1996, Proof-Carrying Code[R]. Technical Report CMU-CS-96-165, November.
Necula G. C.,1997, Proof-carrying code[C]. In POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (New York, NY, USA), pp. 106-119, ACM Press.
Necula G. C.,1998, Compiling with Proofs [D]. PhD thesis, School of Computer Science, Carnegie Mellon Univ. N
Necula G. C. and Lee P., 1998, Safe, Untrusted Agents Using Proof-Carrying Code[J]. Mobile Agents and Security, Giovanni Vigna (Ed.), Lecture Notes in Computer Science, Vol. 1419, Springer-Verlag, Berlin, ISBN 3-540-64792-9.
Necula G. C. and Lee P., 1998, The design and implementation of a certifying compiler[C]. In Proceedings of the 1998 ACM SIGPLAN Conference on Prgramming Language Design and Implementation (PLDI), pp. 333-344.
Ni Z. and Shao Z., 2006, Certified assembly programming with embedded code pointers, in Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06), pp. 320-333.
Oheimb D. V., 2001, Hoare logic for Java in Isabelle/HOL [J]. Concurrency and Computation: Practice and Experience, vol. 13, no. 13, pp. 1173-1214.
Parkinson, M., and Bierman G., 2005. Separation logic and abstraction[C]. SIGPLAN Not.40(1), 247, ISSN 0362-1340.
Paulin-Mohring C., 1993, Inductive definitions in the system Coq: Rules and properties[C]. In Proceedings 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93, Utrecht, The Netherlands, 16-18 March 1993 (M. Bezem and J. F. Groote, eds.), vol. 664, pp. 328-345, Berlin:Springer- Verlag.
Pierce, B. C., 2002, Types and Programming Languages[M]. ISBN 0-262-16209-1,The MIT Press.
Reynolds J. C., 2002, Separation logic: a logic for shared mutable data structures[C]. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74, July.
Reynolds J. C.,2005, An introduction to separation logic. Lecture notes[EB/OL], Available at http://www.cs.cmu.edu/jcr/, Spring.
Rometzky M., Bauer J., Reps T, Sagiv M., Wilhelm and R., 2005, A semantics for procedure local heaps and its abstractions[C]. In Proceedings of the 32th Annual ACM Symposium on Principles of Programming Languages, pages 296-309.
Shao Z, 1997, An overview of the FLINT/ML compiler[C], in Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC'97), (Amsterdam,The Netherlands).
Smith F., Walker D., and Morrisett G., 2000, Alias types[C]. In Proceedings of the 2000 European Symposium on Programming, pages 366-381, Berlin.
The Coq Development Team, 2004, The Coq Proof Assistant Reference Manual- Version V8.0[EB/OL], URL http://coq.inria.fr.
Venet A., 1999, Automatic analysis of pointer aliasing for untyped programs[J]. Science of Computer Programming, 35(2):223-248.
Wright A. K. and Felleisen M., 1994, A syntactic approach to type soundness[J]. Information and Computation, 115(1):38—94.
Xi H. ,1998, Dependent Types in Practical Programming[D]. PhD thesis, Carnegie Mellon University.
Xi H. and Pfenning F., 1999, Dependent types in practical programming[C]. I n Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio,Texas, (New York, NY), pp. 214-227.
Xi H., 2000, Imperative programming with dependent types[C]. In Proceedings of 15th IEEE Symposium on Logic in Computer Science, (Santa Barbara), pp. 375-387.
Xi H, Chen C., and Chen G., 2003., Guarded recursive datatype constructors[C]. In POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (New York, NY, USA), pp. 224-235, ACM Press.
Xi H., 2003. Applied type system (extended abstract) [C]. In the post-workshop proceedings of TYPES 2003, volume 3085 of LNCS, pages 394-408. Springer-Verlag.
Xi H., Zhu D., and Li Y, 2005, Applied Type System with Stateful Views[R], Tech. Rep. BUCS-TR-2005-003, CS Department, Boston University.
Yu D., Hamid N. A., and Shao Z., 2003, Building certified libraries for PCC: Dynamic storage allocation[C]. In Proceedings 12th European Symposium on Programming (ESOP 2003), vol. 2618 of LNCS, pp. 363-379, Springer.
Yu D. and Shao Z., 2004, Verification of safety properties for concurrent assembly code[C]. In Proc. 2004 International Conference on Functional Programming (ICFP'04).
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |