一种基于栈区内存模型的C程序别名判断算法
|
摘要
C语言中的指针导致C程序中会出现表达式别名的情况.在基于演绎推理的程序验证中,使用Hoare逻辑的赋值规则前必须消除断言中的别名.别名增加了程序验证的难度.本文根据C语言的语义提出了一种栈区内存模型,可以精确地跟踪栈区的多种类型的表达式,包括取地址、多级解引用、指针关系运算、结构体和数组等.基于上述内存模型,本文提出了一种判断别名的算法,使得验证工具在使用Hoare逻辑的赋值公理之前可以准确的消除断言中的别名.目前该模型已经在一个名为Safe-C验证器的程序验证工具中实现,并且成功验证了多例经典程序.
Pointers in the C language causes potential aliasing among expressions in a C program. In program verification based on deductive reasoning,the aliases in the assertions must be eliminated before applying the Hoare logic assignment rule. Aliasing increases the difficulty of verifying C programs. Based on C semantics,this paper proposes a memory model that can accurately trace various kind of C expressions in the stack area,including address-taking,multi-level de-reference,pointer relation operation,structure and array,etc. According to this model,this paper proposes an algorithm to identify aliases,which enables the verification tool to accurately eliminate the aliases in the assertions before using the Hoare logic assignment axiom. We have implemented the proposed model in a program verification tool named Safe-C Verifier,which has successfully verified many classic C programs.
Pointers in the C language causes potential aliasing among expressions in a C program. In program verification based on deductive reasoning,the aliases in the assertions must be eliminated before applying the Hoare logic assignment rule. Aliasing increases the difficulty of verifying C programs. Based on C semantics,this paper proposes a memory model that can accurately trace various kind of C expressions in the stack area,including address-taking,multi-level de-reference,pointer relation operation,structure and array,etc. According to this model,this paper proposes an algorithm to identify aliases,which enables the verification tool to accurately eliminate the aliases in the assertions before using the Hoare logic assignment axiom. We have implemented the proposed model in a program verification tool named Safe-C Verifier,which has successfully verified many classic C programs.
引文
[1]Landi William.Undecidability of static analysis[J].Acm Letters on Programming Languages&Systems,1992,1(4):323-337.
[2]Ramalingam G.The undecidability of aliasing[J].Acm Transactions on Programming Languages&Systems,1994,16(5):1467-1471.
[3]Visser W,Havelund K,Brat G,et al.Model checking programs[J].Automated Software Engineering,2003,10(2):203-232.
[4]Necula G C.ProofCarrying Code.Design and Implementation[M].Proof and SystemReliability,Springer Netherlands,Dordrecht,2002.
[5]Hoare C A R.An axiomatic basis for computer programming[J].Communications of the Acm,1969,12(1):53-56.
[6]Reynolds J C.Separation logic:a logic for shared mutable data structures[C].Logic in Computer Science Symposium on,IEEE,2002:55-74.
[7]Moura L D,Bjrner N.Z3:an efficient SMT solver[C].International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Springer,Berlin,Heidelberg,2008:337-340.
[8]Zhang Zhi-tian,Li Zhao-peng,Chen Yi-yun,et al.An automatic program verifier for pointerC:design and implementation[J].Journal of Computer Research and Development,2013,50(5):1044-1054.
[9]Li Zhao-peng,Zhang Yu,Chen Yi-yun.A shape graph logic and a shape system[J].Journal of Computer Science and Technology,2013,V28(6):1063-1084.
[10]Cadar C,Twohey P,Ganesh V,et al.EXE:a system for automatically generating inputs of death using symbolic execution[J].Stain Technology,2006,51(3):199-201.
[11]Godefroid P,Klarlund N,Sen K.DART:directed automated random testing[J].Acm Sigplan Notices,2005,40(6):213-223.
[12]Baudin P,Filliatre J C,MarchéC,et al.ACSL:ANSI/ISO Cspecification language[OL/J].http://citeseerx.ist.psu.edu/view doc/summary?doi=10.1.1.365.4451.
[13]Feng Feng,Luo Qi-ming,Chen Yi-yun.Formal verification of stack pointer programs[J].Journal of Chinese Computer Systems,2017,38(5):936-940.
[14]Cohen E,Moskal M,Schulte W,et al.Local verification of global Invariants in concurrent programs[C].Computer Aided Verification,International Conference,CAV 2010,Edinburgh,Uk,DBLP,2010.
[15]Boldo S,Jourdan J H,Leroy X,et al.Verified compilation of floating point computations[J].Journal of Automated Reasoning,2015,54(2):135-163.
[16]Bart Jacobs F P.The verifast program verifier[J].Cw Reports,2008:304-311.
[17]Barnett M,Leino K R M,Schulte W.The spec#programming system:an overview[C].International Workshop on Construction and Analysis of Safe,Secure,and Interoperable Smart Devices,Springer,Berlin,Heidelberg,2004.
[8]张志天,李兆鹏,陈意云,等.一个程序验证器的设计和实现[J].计算机研究与发展,2013,50(5):1044-1054.
[9]李兆鹏,张昱,陈意云.形状图逻辑和形状图系统[J].计算机科学与技术学报,2013,V28(6):1063-1084.
[13]冯峰,罗奇鸣,陈意云.栈指针程序的形式验证[J].小型微型计算机系统,2017,38(5):936-940.
[2]Ramalingam G.The undecidability of aliasing[J].Acm Transactions on Programming Languages&Systems,1994,16(5):1467-1471.
[3]Visser W,Havelund K,Brat G,et al.Model checking programs[J].Automated Software Engineering,2003,10(2):203-232.
[4]Necula G C.ProofCarrying Code.Design and Implementation[M].Proof and SystemReliability,Springer Netherlands,Dordrecht,2002.
[5]Hoare C A R.An axiomatic basis for computer programming[J].Communications of the Acm,1969,12(1):53-56.
[6]Reynolds J C.Separation logic:a logic for shared mutable data structures[C].Logic in Computer Science Symposium on,IEEE,2002:55-74.
[7]Moura L D,Bjrner N.Z3:an efficient SMT solver[C].International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Springer,Berlin,Heidelberg,2008:337-340.
[8]Zhang Zhi-tian,Li Zhao-peng,Chen Yi-yun,et al.An automatic program verifier for pointerC:design and implementation[J].Journal of Computer Research and Development,2013,50(5):1044-1054.
[9]Li Zhao-peng,Zhang Yu,Chen Yi-yun.A shape graph logic and a shape system[J].Journal of Computer Science and Technology,2013,V28(6):1063-1084.
[10]Cadar C,Twohey P,Ganesh V,et al.EXE:a system for automatically generating inputs of death using symbolic execution[J].Stain Technology,2006,51(3):199-201.
[11]Godefroid P,Klarlund N,Sen K.DART:directed automated random testing[J].Acm Sigplan Notices,2005,40(6):213-223.
[12]Baudin P,Filliatre J C,MarchéC,et al.ACSL:ANSI/ISO Cspecification language[OL/J].http://citeseerx.ist.psu.edu/view doc/summary?doi=10.1.1.365.4451.
[13]Feng Feng,Luo Qi-ming,Chen Yi-yun.Formal verification of stack pointer programs[J].Journal of Chinese Computer Systems,2017,38(5):936-940.
[14]Cohen E,Moskal M,Schulte W,et al.Local verification of global Invariants in concurrent programs[C].Computer Aided Verification,International Conference,CAV 2010,Edinburgh,Uk,DBLP,2010.
[15]Boldo S,Jourdan J H,Leroy X,et al.Verified compilation of floating point computations[J].Journal of Automated Reasoning,2015,54(2):135-163.
[16]Bart Jacobs F P.The verifast program verifier[J].Cw Reports,2008:304-311.
[17]Barnett M,Leino K R M,Schulte W.The spec#programming system:an overview[C].International Workshop on Construction and Analysis of Safe,Secure,and Interoperable Smart Devices,Springer,Berlin,Heidelberg,2004.
[8]张志天,李兆鹏,陈意云,等.一个程序验证器的设计和实现[J].计算机研究与发展,2013,50(5):1044-1054.
[9]李兆鹏,张昱,陈意云.形状图逻辑和形状图系统[J].计算机科学与技术学报,2013,V28(6):1063-1084.
[13]冯峰,罗奇鸣,陈意云.栈指针程序的形式验证[J].小型微型计算机系统,2017,38(5):936-940.