计算机研究与发展 ISSN1000-1239/CN11-1777/TP Journal of Computer Research and Development 50(5):1044-1054,2013 一个程序验证器的设计和实现 张志天李兆鹏陈意云刘刚 (中国科学技术大学计算机科学技术学院合肥230026) (中国科学技术大学苏州研究院软件安全实验室江苏苏州215123) (zpli@ustc.edu.cn) An Automatic Program Verifier for PointerC:Design and Implementation Zhang Zhitian,Li Zhaopeng,Chen Yiyun,and Liu Gang (School of Computer Science and Technology.University of Science and Technology of China.Hefei 230026) (So ftware Security Laboratory.Suzhou Institute for Advanced Study.University of Science and Technology of China, Suzhou.Jiangsu 215123) Abstract 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. Key words program verification;Hoare logic;shape graph logic;program analysis;separation logic 摘要形式验证是提高软件可信程度的重要方法，基于逻辑推理对程序性质进行严格的自动证明是当 前的研究热点，但尚无可供工业界使用的产品，其根源在于自动定理证明方面的困难.介绍在通过程序 分析建立起各程序点的形状图的基础上，如何利用形状图提供的信息来支持程序验证的方法，提出一种 利用形状图信息来消除访问路径别名，使得指针程序中非指针部分的性质仍然可以用Hore逻辑来进 行验证的方法，并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下，易变数据结构上 数据性质的描述和验证方法，另外，介绍所设计并实现的基于上述方法的PointerC语言的程序验证器 的原型.它不仅能自动验证操作易变数据结构程序的性质，也能自动验证使用一雏数组的程序的性质. 关键词程序验证；Hoare逻辑；形状图逻辑；程序分析；分离逻辑 中图法分类号TP301 收稿日期：2010-11-29：修回日期：2012-12-10 基金项目：国家自然科学基金项日(61170018,61003043) 通信作者：李兆鹏(zpli@ustc.edu.cm)书 ! " # $ % & ' ( !""#$%%%&$'()!*#$$&$+++!,- ./01234/5*/670891:9;931<=32>?9@94/76928 A%!A"#$%BB$%AB$'%$( !"#$#'%$%C$$C')%%&#$#'%$'C$'C$% '()*#)*+,-./012!D$$+%%$E$D$%%(%B(" +,-.#345!F74G"0;8<H9>0H<2" /0123456789:; !"# $%& '() * + !6)-.789.!"#-.78.: ;< '(%%'D" !6)-.789.=>$%:?@ABCDE F==> '$A$'(" !F74G"0;8<H9>0H<2" !"!#$%&'$()*+%,+'&-.+(/(.+/%+*%("$.+0#1.2(,"'"34&56.&."$'$(%" I=32JI=G8G32$KGI=3/792J$*=92LGM02$32>KG0N32J !!"#$$%$&'$()*+,-!".,/",0/12,"#/$%$34$5/.6,-7.+4$&!".,/",0/12,"#/$%$34$&'#./0$8,&,.'(%%'D" !!$&+90-,!,"*-.+4:0;$-0+$-4$!*<#$*=/7+.+*+,&$->160/",1!+*14$5/.6,-7.+4$&!".,/",0/12,"#/$%$34$&'#./0$ !*<#$*$?.0/37*'$A$'(" !72$+')$ O/1634@91G5G<38G/2G;363P/1698=/>8/G671/@98=9>9792>3QG4G8M/5;/58R319HS29/58=9 =/819;931<=3193;G;308/638G<71/J136 @91G5G<38G/2Q3;9>/24/JG<34G259192<9H"/5318=919G;2/ 71/>0<8R=G<=<32Q90;9>>G19<84MG28=9G2>0;81G9;$32>8=91//8/58=G;71/Q4964G9;G28=9;4/R >9@94/7692832>>G55G<048G9;/5308/6389>8=9/19671/@G2JHS013771/3<=G;Q3;9>/28=9/Q;91@38G/2 8=3871/J136 3234M;G; 698=/>;<32 Q90;9>G2</449<8G2JJ4/Q34G25/1638G/28/;077/1871/J136 @91G5G<38G/2HT9Q0G4>;=379J137=;3893<=71/J1367/G28G28=971/J1363234M;G;7=3;9HU 698=/>G; 71/7/;9>$R=G<=0;9;19J0431V/3194/JG<1049;8/193;/23Q/083;;GJ269282/8>934G2JRG8=7/G2891; G23*&4GW971/J1366G2J432J03J9H"0<=1049;RG44Q93774G9>3589134G3;G2JG;94G6G2389>0;G2J8=9 G25/1638G/2/5;=379J137=;H,=9;/02>29;;/58=94/JG<;M;896=3;Q99271/@9>HO018=916/19$32 3771/3<=G;719;9289>8/@91G5M>383</2;813G28;/26083Q49>383;810<8019;RG8=/080;G2J0;91&>95G29> 719>G<389;HU71/8/8M79/5/0171/J136@91G5G91=3;Q992G674969289>5/18=9-/G2891*71/J1366G2J 432J03J9HT9=3@90;9>G8G28=9@91G5G<38G/2/571/J136;632G70438G2J19<01;G@9>383;810<8019;$;0<= 3;4G;8;32>8199;$32>71/J136;>934G2JRG8=/29&>G692;G/23113M;H 8.9:%+32 71/J136@91G5G<38G/2%V/3194/JG<%;=379J137=4/JG<%71/J1363234M;G;%;973138G/24/JG< < = !"#$%&'()*+,-./012!3456789,:;<=>?@.AB$C%D E.FGHI!JKL*MNOPQR.ST!UVWX4ABY8$C1Z.[\H]^X_`,: abcdef,:I.!gh.3ij!klmR!gh&M.+nopq,:#$.12H&rst mR!gh+nouvwxyz{|!Q}~,:€~‚a.;<ƒ„*…R V/31956o= >#$.12!†$C‡ˆ12.*‰;HŠ&rstX‹QRAYŒŽ.‘!’•j •;<.™š#$12H›œ!]^žŸ† ¡.34j™12. -/G2891*¢£.,:#$¤ .¥¦H§‹¨©AB#$ª«’•,:.;<!¬©AB#$QRs­®.,:.;<H >?@ ,:#$"V/31956"!gh56",:ab"a¯56 ABCDEF ,-(%$