一个程序验证器的设计和实现
|
摘要
形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质.
Formal verification is a major method to improve the dependability of software.One of the hot research areas is automatic program verification based on logical inference.So far there is no product which can be used directly in the industries,and the root of this problem lies in the slow development and difficulties of automated theorem proving.Our approach is based on the observation that program analysis methods can be used in collecting global information to support program verification.We build shape graphs at each program point in the program analysis phase.A method is proposed,which uses regular Hoare logic rules to reason about assignment not dealing with pointers in a C-like programming language.Such rules will be applied after aliasing is eliminated using the information of shape graphs.The soundness of the logic system has been proved.Furthermore,an approach is presented to verify data constraints on mutable data structures without using user-defined predicates.A prototype of our program verifier has been implemented for the PointerC programming language.We have used it in the verification of programs manipulating recursive data structures,such as lists and trees,and programs dealing with one-dimension arrays.
Formal verification is a major method to improve the dependability of software.One of the hot research areas is automatic program verification based on logical inference.So far there is no product which can be used directly in the industries,and the root of this problem lies in the slow development and difficulties of automated theorem proving.Our approach is based on the observation that program analysis methods can be used in collecting global information to support program verification.We build shape graphs at each program point in the program analysis phase.A method is proposed,which uses regular Hoare logic rules to reason about assignment not dealing with pointers in a C-like programming language.Such rules will be applied after aliasing is eliminated using the information of shape graphs.The soundness of the logic system has been proved.Furthermore,an approach is presented to verify data constraints on mutable data structures without using user-defined predicates.A prototype of our program verifier has been implemented for the PointerC programming language.We have used it in the verification of programs manipulating recursive data structures,such as lists and trees,and programs dealing with one-dimension arrays.
引文
[1]Lin Huimin,Zhang Wenhui.Model checking:Theory,methods and applications[J].Acta Electronica Sinica,2002,30(12A):1907-1912(in Chinese)(林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(12A):1907-1912)
[2]Hoare C A R.An axiomatic basis for computer programming[J].Communications of the ACM,1969,12(10):576-585
[3]Paulson L C.Isabelle:A Generic Theorem Prover[M].Berlin:Springer,1994:1-300
[4]The Coq Development Team.The Coq proof assistant reference manual,Version8.2[OL].[2009-08-01].http://coq.inria.fr
[5]Aleksandar N,Morrisett G,Shinnar A,et al.Ynot:Dependent types for imperative programs[C]//Proc of the13th ACM SIGPLAN Int Conf on Functional Programming(ICFP'08).New York:ACM,2008:229-240
[6]Barnett M,Rustan M,Leino M,et al.The spec#programming system:An overview[G]//LNCS3362:Proc of Int Workshop Construction and Analysis of Safe,Secure,and Interoperable Smart Devices(CASSIS2004).Berlin:Springer,2004:49-69
[7]Flanagan C,Leino K R M,Lillibridge M,et al.Extended static checking for Java[C]//Proc of the Conf on Programming Language Design and Implementation(PLDI'02).New York:ACM,2002:234-245
[8]Berdine J,Calcagno C,O'Hearn P W.Smallfoot:Modular automatic assertion checking with separation logic[G]//LNCS4111:Proc of Formal Methods for Components and Objects(FMCO2005).Berlin:Springer,2005:115-137
[9]Distefano D,Parkinson M J.jStar:Towards practical verification for Java[C]//Proc of ACM SIGPLAN Int Conf on Object-Oriented Programming,Systems,Languages,and Applications(OOPSLA2008).New York:ACM,2008:213-226
[10]Carter G,Monahan R,Morris J M.Software refinement with perfect developer[C]//Proc of the3rd IEEE Int Conf on Software Engineering and Formal Methods(SEFM2005).Piscataway,NJ:IEEE,2005:363-372
[11]Reynolds J C.Separation logic:A logic for shared mutable data structures[C]//Proc of the17th Annual IEEE Symp on Logic in Computer Science(LICS2002).Piscataway,NJ:IEEE,2002:55-74
[12]Berdine J,Calcagno C,O'Hearn P W.A decidable fragment of separation logic[G]//LNCS3328:Proc of the24th Int Conf on Foundations of Software Technology and Theoretical Computer Science(FSTTCS2004).Berlin:Springer,2004:97-109
[13]Moura L D,Bjrner N.Z3:An efficient SMT solver[G]//LNCS4963:Proc of Conf on Tools and Algorithms for the Construction and Analysis of Systems(TACAS2008).Berlin:Springer,2008
[14]Li Zhaopeng,Zhang Yu,Chen Yiyun.Shape graph logic and a shape system[OL].[2012-12-05].http://ssg.ustcsz.edu.cn/SGL
[15]Liu Gang,Chen Yiyun,Zhang Zhitian.Automatic inference of loop invariant shape graphs[J].Chinese Journal of Electronic Technology,2011(8):4-6(in Chinese)(刘刚,陈意云,张志天.循环不变形状图的自动推断[J].电子技术,2011(8):4-6)
[16]Necula G.Proof-carrying code[C]//Proc of the24th ACM Symp on Principles of Programming Languages(POPL'97).New York:ACM,1997:106-119
[17]Bornat R.Proving pointer programs in Hoare logic[G]//LNCS1837:Proc of the5th Int Conf on Mathematics of Program Construction(MPC2000).Berlin:Springer,2000:102-126
[18]Kroening D,Strichman O.Decision Procedures:An Algorithmic Point of View[M].Berlin:Springer,2008
[19]Zhang Zhitian,Li Zhaopeng,Chen Yiyun,et al.The verifier prototype system of PointerC based on the shape graph logic and shape system[OL].[2012-12-05].http://ssg.ustcsz.edu.cn/content/shape-graph-logic
[20]Jacobs B,Piessens F.The VeriFast program verifier.TR CW-520[R].Flanders,Belgium:Department of Computer Science,Katholieke Universiteit Leuven,2008
[21]Chen Yiyun,Li Zhaopeng,Wang Zhifang,et al.A pointer logic for safety verification of pointer programs[J].Journal of Software,2010,21(3):124-137(in Chinese)(陈意云,李兆鹏,王志芳,等.一种用于指针程序验证的指针逻辑[J].软件学报,2010,21(3):124-137)
[22]Chin W,David C,Nguyen H H,et al.Automated verification of shape,size and bag properties[C]//Proc of the12th IEEE Int Conf on Engineering of Complex Computer Systems(ICECCS2007).Piscataway,NJ:IEEE,2007:307-320
[23]Yang H,Lee O,Berdine J,et al.Scalable shape analysis for systems code[C]//Proc of the20th Int Conf on Computer Aided Verification(CAV2008).New York:ACM,2008:385-398
[24]Brotherston J,Bornat R,Calcagno C.Cyclic proofs of program termination in separation logic[C]//Proc of the ACM SIGPLAN—SIGACT Symp on Principles of Programming Languages(POPL2008).New York:ACM,2008:739-782
[25]Calcagno C,Parkinson M J,Vafeiadis V.Modular safety checking for fine-grained concurrency[G]//LNCS4634:Proc of the14th Int Static Analysis Symp(SAS2007).Berlin:Springer,2007:233-248
[26]Gotsman A,Berdine J,Cook B,et al.Local reasoning for storable locks and threads[G]//LNCS4807:Proc of the5th ASIAN Symp on Programming Languages and Systems(APLAS2007).Berlin:Springer,2007:19-37
[27]Haack C,Hurlin C.Separation logic contracts for a Java-like language with fork/join[G]//LNCS5140:Proc of the12th Int Conf on Algebraic Methodology and Software Technology(AMAST2008).Berlin:Springer,2008:199-215
[2]Hoare C A R.An axiomatic basis for computer programming[J].Communications of the ACM,1969,12(10):576-585
[3]Paulson L C.Isabelle:A Generic Theorem Prover[M].Berlin:Springer,1994:1-300
[4]The Coq Development Team.The Coq proof assistant reference manual,Version8.2[OL].[2009-08-01].http://coq.inria.fr
[5]Aleksandar N,Morrisett G,Shinnar A,et al.Ynot:Dependent types for imperative programs[C]//Proc of the13th ACM SIGPLAN Int Conf on Functional Programming(ICFP'08).New York:ACM,2008:229-240
[6]Barnett M,Rustan M,Leino M,et al.The spec#programming system:An overview[G]//LNCS3362:Proc of Int Workshop Construction and Analysis of Safe,Secure,and Interoperable Smart Devices(CASSIS2004).Berlin:Springer,2004:49-69
[7]Flanagan C,Leino K R M,Lillibridge M,et al.Extended static checking for Java[C]//Proc of the Conf on Programming Language Design and Implementation(PLDI'02).New York:ACM,2002:234-245
[8]Berdine J,Calcagno C,O'Hearn P W.Smallfoot:Modular automatic assertion checking with separation logic[G]//LNCS4111:Proc of Formal Methods for Components and Objects(FMCO2005).Berlin:Springer,2005:115-137
[9]Distefano D,Parkinson M J.jStar:Towards practical verification for Java[C]//Proc of ACM SIGPLAN Int Conf on Object-Oriented Programming,Systems,Languages,and Applications(OOPSLA2008).New York:ACM,2008:213-226
[10]Carter G,Monahan R,Morris J M.Software refinement with perfect developer[C]//Proc of the3rd IEEE Int Conf on Software Engineering and Formal Methods(SEFM2005).Piscataway,NJ:IEEE,2005:363-372
[11]Reynolds J C.Separation logic:A logic for shared mutable data structures[C]//Proc of the17th Annual IEEE Symp on Logic in Computer Science(LICS2002).Piscataway,NJ:IEEE,2002:55-74
[12]Berdine J,Calcagno C,O'Hearn P W.A decidable fragment of separation logic[G]//LNCS3328:Proc of the24th Int Conf on Foundations of Software Technology and Theoretical Computer Science(FSTTCS2004).Berlin:Springer,2004:97-109
[13]Moura L D,Bjrner N.Z3:An efficient SMT solver[G]//LNCS4963:Proc of Conf on Tools and Algorithms for the Construction and Analysis of Systems(TACAS2008).Berlin:Springer,2008
[14]Li Zhaopeng,Zhang Yu,Chen Yiyun.Shape graph logic and a shape system[OL].[2012-12-05].http://ssg.ustcsz.edu.cn/SGL
[15]Liu Gang,Chen Yiyun,Zhang Zhitian.Automatic inference of loop invariant shape graphs[J].Chinese Journal of Electronic Technology,2011(8):4-6(in Chinese)(刘刚,陈意云,张志天.循环不变形状图的自动推断[J].电子技术,2011(8):4-6)
[16]Necula G.Proof-carrying code[C]//Proc of the24th ACM Symp on Principles of Programming Languages(POPL'97).New York:ACM,1997:106-119
[17]Bornat R.Proving pointer programs in Hoare logic[G]//LNCS1837:Proc of the5th Int Conf on Mathematics of Program Construction(MPC2000).Berlin:Springer,2000:102-126
[18]Kroening D,Strichman O.Decision Procedures:An Algorithmic Point of View[M].Berlin:Springer,2008
[19]Zhang Zhitian,Li Zhaopeng,Chen Yiyun,et al.The verifier prototype system of PointerC based on the shape graph logic and shape system[OL].[2012-12-05].http://ssg.ustcsz.edu.cn/content/shape-graph-logic
[20]Jacobs B,Piessens F.The VeriFast program verifier.TR CW-520[R].Flanders,Belgium:Department of Computer Science,Katholieke Universiteit Leuven,2008
[21]Chen Yiyun,Li Zhaopeng,Wang Zhifang,et al.A pointer logic for safety verification of pointer programs[J].Journal of Software,2010,21(3):124-137(in Chinese)(陈意云,李兆鹏,王志芳,等.一种用于指针程序验证的指针逻辑[J].软件学报,2010,21(3):124-137)
[22]Chin W,David C,Nguyen H H,et al.Automated verification of shape,size and bag properties[C]//Proc of the12th IEEE Int Conf on Engineering of Complex Computer Systems(ICECCS2007).Piscataway,NJ:IEEE,2007:307-320
[23]Yang H,Lee O,Berdine J,et al.Scalable shape analysis for systems code[C]//Proc of the20th Int Conf on Computer Aided Verification(CAV2008).New York:ACM,2008:385-398
[24]Brotherston J,Bornat R,Calcagno C.Cyclic proofs of program termination in separation logic[C]//Proc of the ACM SIGPLAN—SIGACT Symp on Principles of Programming Languages(POPL2008).New York:ACM,2008:739-782
[25]Calcagno C,Parkinson M J,Vafeiadis V.Modular safety checking for fine-grained concurrency[G]//LNCS4634:Proc of the14th Int Static Analysis Symp(SAS2007).Berlin:Springer,2007:233-248
[26]Gotsman A,Berdine J,Cook B,et al.Local reasoning for storable locks and threads[G]//LNCS4807:Proc of the5th ASIAN Symp on Programming Languages and Systems(APLAS2007).Berlin:Springer,2007:19-37
[27]Haack C,Hurlin C.Separation logic contracts for a Java-like language with fork/join[G]//LNCS5140:Proc of the12th Int Conf on Algebraic Methodology and Software Technology(AMAST2008).Berlin:Springer,2008:199-215