（计算机软件与理论专业论文）指针逻辑的扩展与应用.pdf

摘要 摘要 在信息时代，计算机软件技术得到了广泛的应用。然而，随着软件功能越 来越强大，软件本身也变得愈发复杂，软件的可靠性和安全性越来越难以得到 保障。在通常使用的c ，c + + 或者j a v a 语言中，为了使程序能够高效运行，指 针或者引用在程序中大量使用。但是指针的灵活使用很容易引起错误，比如空 指针或者悬空指针引用，内存泄露等。这些错误不仅难以发现，如果一旦发生 可能导致系统崩溃。而且，这些程序漏洞可能被黑客加以利用。另一方面，指 针错误之所以难以被发现，是因为不同指针之间存在可能的别名关系，即是两 个语法上不同的名字在运行的时候可能引用同一个内存地址。修改一个名字对 应的值，别的名字所对应的值可能也会随之改变，给程序调试和程序推理带来 很大的困难。因此，带有指针程序的安全性在软件安全研究中占有重要位置。 由于指针程序安全研究具有很大的挑战性，工业界常用的软件测试方法无 法完全保证错误不会发生，因而指针程序性质证明方法成为当前研究热点。 而现有的证明方法，要么需要显式引入堆或栈等高级语言语法之外的概念来 刻画程序的运行状态，要么生成的验证条件太过于复杂而不能够自动证明， 而需要程序员手工证明。堆和栈的描述需要知道确切的内存地址，但是具有 同构结构的堆是不可以区分的。而无存储模型方法则克服了上述所有困难， 不需要显式引入堆栈概念，而其良好性质保证可以被自动机实现，因而证明 可以自动。指针逻辑在本质上是基于无存储模型方法，但是当前还具有很多 不足。当前指针逻辑缺少抽象模型描述，导致了指针逻辑规则都是由算法风 格函数辅助构成，这使得难以看清楚指针逻辑本质。而且，当前指针逻辑支 持的指针特征较少，虽然断言语言支持符号访问路径，用户自定义谓词和描 述性谓词，但是其实现p l c c ( v 1 )( p o i n t e rl o g i cc e r t i f y i n gc o m p i l e r ，简称 为p l c c ，v 1 表示v e r s i o n1 ，后面的v 2 表示v e r s i o n2 ) 的推理并不支持。最重 要的是，p l c c ( v 1 ) 生成的验证条件并不能自动证明，而需要程序员通过交 互式定理证明器c o q 来完成证明。 基于上述考虑，本文在访问路径相等概念上提出一个无存储模型，研究了 该模型的各种性质，例如右规则性，前缀闭包性等。同时，本文专注于无存储 模型上的指针逻辑断言的良型性，继而重新阐述了指针逻辑推理规则。为了 使指针逻辑能够验证更大范围的程序，本文提出了针对指针逻辑的框架规则 ( f r a m er u l e ) 和函数调用规则。此外，本文在原有指针逻辑基础上，扩展源语 言和断言语言来支持指针算术，然后在方便模块化实现前提下扩展指针逻辑规 则来保障指针算术的安全。原来指针逻辑中的集合是无名集合，而无名集合不 能处理含有某些情况下的函数调用的程序，因而本文提出带标签的集合可以适 摘要 用于任意函数调用的验证。在实现方面，本文根据无存储模型性质设计了实现 指针逻辑规则的自动推理算法，并提出了展开机制来处理断言语言支持用户自 定义谓词和描述性谓词。最后，本文工作均在p l c c ( v 2 ) 的前端中实现。 本文的主要特色和贡献为： 本文提出了一个比己存在无存储模型更有效更简洁的无存储模型。此模型 不仅继承了已存在无存储模型的优点，而且克服了其冗余多，表示代价高 的缺点。 本文完善了指针逻辑，在抽象模型上以一种简单更为容易理解的方式重新 阐述指针逻辑推理规则。由于抽象模型没有传统无存储模型的冗余，花费 代价大等缺点，因而本文可以发现以前指针逻辑( c h e ne ta 1 ，2 0 0 7 a b ) 规 则中具有一个漏洞：以前指针逻辑所定义的n o l e a k 函数在某些时候会将某 些正确程序误认为会出现内存错误而拒绝。本文给出修正此漏洞的规则， 同时这也反映了建立抽象模型的必要性，因为以前的指针逻辑规则是基于 一些复杂的算法风格的辅助函数，并且导致难以看清楚指针逻辑的本质。 本文扩展了指针逻辑。相比扩展前的指针逻辑，本文扩展了指针逻辑在局 部推理的规则、扩展支持在动态数组上的指针算术以及利用带标签的集合 来验证任意函数调用的扩展，这样指针逻辑就能够在更大范围内保障程序 的安全。 本文设计了实现指针逻辑规则的算法和提出了展开技术来实现谓 词推理自动化，并将其应用到自动验证工具p l c c ( v 2 ) 前端实现 上。相比p l c c ( v 1 ) 需要程序员利用c o q 手工证明其生成的验证条 件，p l c c ( v 2 ) 可以自动完成各种推理证明而不需要程序员手工干预。 同时而可以利用谓词展开技术验证很多非平凡的指针程序，例如在单向链 表，双向循环链表，树等常用数据结构上的操作，其中包括被认为是指针 形式化指标的s c h o r r - w 撕t e 树遍历算法。 关键词：软件安全程序性质证明无存储内存模型指针逻辑验证框架 i i a b s t r a c t a b s t r a c t n o w a d a 归，s o r w a r et e c h n i q u ei s 丽d e l yu s e d h o w e v e r ，t h ea r c h i t e c t u r eo f s o f t w a r ei sm o r ea n dm o r ec o m p h c a t e da si t ss i z eg r o w s ，a n di ti sm o r ea n dm o r e d 瓶c u l tt og u a r a n t e ei t ss a f e t y i nt h ep r o g m m m i n g1 a n g u a g es u c ha sc ，c + + o rj a a ，p o i n t e r so rr e f e r e n c e sa r ec o m m o n l yu s e dt oa u c h i e v eh i 曲p e r f o r m a n c e b u tt h ef l e x i b i l i t yo fp o i n t e r si sa p tt oc a u s ee r r o r ss u c ha sn m lp o i n t e rr e f e r e n c e j l a n g l i n gp o i n t e rd e f e r e n c ea n dm e m o r yl e a l ( sw h i c ha r ed i m c u l tt o 丘n d o n c e t h e s ee r r o r so c c u r ，t h es y s t e mw o u l dc r a s h a n dm o r es e r i o u s l y t h e yc a nb e ta ：k e na d v a n t a g eo fb yh a c k e r s o nt h eo t h e r h a n d ，t h er e a s o nt h a tp o i n t e re r r o r s a r eh a r dt od e t e c ti sb e c a l l s ed i s t i n c tp o i n t e r sm i g h tb ea l i a l s e dt oe a c ho t h e r ，i e ， t w od i 髓r e n tn a m e sc o u l dr e f e rt ot h es a m em e m o 盯a d d r e s s m o d i 肌n gt h ev 出u e o fo n ep o i n t e rc o u l da 骶c tt h ev a l u eo ft h eo t h e r ，w h i c he x h i b i t sg r e a td i m c u l t i e s f o rd e b u g g i n ga n dr e a s o n i n g a sar e s u l t ，t h er e s e a r c ho nt h es a f 色t yo fp o i n t e r p r o g r a m sp l a y sa i li m p o r t a n tr o l ei i ls o f t w a r es e c u r i t y a st h er e s e a r c ho fp o i n t e rp r o f a ms a f e t yi sc h a l l e n g i n g ，w h j l es o f t w a r et e s t c a nn o tg u a r a n t e ei t ss o u n d n e s s ，p o i n t e rp r o g r a mv e r i n c a t i o nb e c o m e sah o tr e s e a l r c ht o p i c h o w 它v e r ，t h ec u r r e n tv e r i f i e a t i o nm e t h o d sb e a rl o t so fd e f e c t s e i t h e r t h e yh w r et oi n t r o d u c es t a c ko rh e 印w h i c hi sn o tt h es y n 乞a xo ft h ep r o g r a m m i n g l a n g u a g et oc a p t u r et h ep r o g r a m m i n gr u n n i n gs t a t e ，o rt h e yg e n e r a t ec o m p l i c a t e d v e r i 丘c a t i o nc o n d i t i o n sw h i c hc a nn o tb ea u t o m a t e d l yp r o v i 耐t h ei n t r o d u c t i o no f s t a c ka n dh e a pn e e d st ok n o wt h ee x a c tm e m o r ya d d r e s s ，b u ti s o m o r p h i ch e a p s a r ei n d i s t i n g u i s h a b l e s t o r e l e s sm e m o r ym o d e l sn o to n l yg e to v e rt h e s ep r o b l e i n s ，b u ta l s ol e a dt 0a u t o m a t e dv e r i f i c a t i o nb e c a u s eo fi t sn i c ep r o p e r t i e s i n e s s e n c ep o i n t e rl o g i ci sb a s e do nt h em e t h o do fs t o r e l e s sm e m o r ym o d e l s ，b u ts t i l l l a u c l c st h ed e s c r i p t i o no fa na b s t r a c ts t o r e l e s sm o d e l ，w h i c hl e a d st ot h ea l g o r i t k m i cs t y l ed e s c r i p t i o no ft h ei n f e r e n c er u l e s ，1 1 i n d e r i n gt h ee x p l o r a t i o no fp o i n t e r l o g i ce s s e n c e f 、l r t h e r m o r e ，p o i n t e rl o g i cl a c ks u p p o r tf o rp o i n t e ra r i t h m e t i c ，a n d t h ei m p l e m e n t a t i o npl c c ( v 1 ) g e n e r a t e sv e r i f i c a t i o nc o n d i t i o n sw h i c hh a st ob e p r o v e di ni n t e r a c t i v et h e o r e mp r o v ei nc oq b a u s e do nt h ea b o v ec o 璐i d e r a t i o n ，t h i st h e s i sp r o p o s e sas t o r e l e s sm o d e la n d p r o b e si n t oi t sp r o p e r t i e ss u c ha sr i g h tr e g u l a r i t y p r e 叔c l o s u r ee t c m e a r l w h i l e i t h et h e s i sf o c u s e so nt h ew e l l - f o r m e d n e s so fp o i n t e rl o g i c sa s s e r t i o nl a n g u a g e ， a n dr e p h r a s e sp o i n t e rl o g i c si n f e r e n c er u l e s i no r d e rt ov e r i f y 研d e l yu s e dd a t a s t r u c t u r e s ，t h et h e s i sp r o p o s e sf r a m er u l ei np o i n t e rl o 酉ca n dt h er u l ef o rf u n c i i i a b s t r a c t t i o nc a l l f i u r t h e r m o r e ，t h es o u r c e1 a n g u a g ea n da s s e r t i o nl a n g u a g ea r ee x t e n d e d t os u p p o r tp o i n t e ra r i t h m e t i c ，w h i l ep o i n t e rl o g i cr u l e sa r ee x t e n d e dt oe n s u r e t h es a f e t yo fp o i n t e ra u r i t h m e t i c f o r m e r l yi np o i n t e rl o g i ct h es e t s 缸eu n n a m e d w 1 1 i c hc a nn o th a n d l ep r o g r a m sc o n t a i n i n gf u n c t i o nc a l l su n d e rs o m ec i r c u m - s t a n c e s t h u st h i st h e s i sp r o p o s e sp o i n t e rl o g i cw i t h1 2 l b e l j st ov e r i f yp r o g r a i n s w i t ha r b i t r a 珂f u n c t i o nc a l l a st ot h ei m p l e m e n t a t i o n ，a u t o m a t i cd e d u c t i o na l g o r i t h m sf o rp o i n t e rl o g i cr u l e sa r ed e s i g n e da n dt h eu n f o l d i n gm e c h a n i s ma r e p r o p o s e dt od e a lw i t ht h eu s e r d e f i n e dp r e d i c a 七e s a 七1 a s t ，t h e r o r ki nt h e s i si s i m p l e m e i l t e di np l c c ( v 2 ) t h em a i nc o n t r i b u t i o n sa n dc h a r a c t e r i s t i c so ft h i sd i s s e r t a t i o na r e ： i tp r e s e n t sam o r ee e t i v es t o r e l e s sm e m o r ym o d e lw h i c hn o to n l ye n j o y s t h en i c ep r o p e r t i e so fe x i s t i n gs t o r e l e s sm o d e l s ，b u ta l s oo v e r c o m e st h e i r s h o r t c o m i n g ss u c ha sr e d u n d a n c ya n dh i g hc o s t s i tp e r f 色c t sp o i i l t e rl o g i cb yr e p h r a s i n gp o i n t e rl o g i cr u l e so nt h ea 南s t r a c t m o d e l b e c a u s et h em o d e li ss i m p l ea n de m c i e n t ，t h et h e s i sc a nd i s c o 、厂e ra 丑a wi nf b r m e rp o i n t e rl o g i cr u l e s ：t h en o l e a kf h n c t i o n 、o u l dr e j e c tc o r r e c t p r o g r a m si ns o m ec i r c u m s t a n c e s ，w h i l ei nt h i st h e s i st h er u l ei sc o r r e c t e d i te x t e n d sp o i n t e rl o g i c c o m p a r e dt of o r m e rp o i n t e rl o g i c ，t h et h e s i se x - t e n d sp o i n t e r1 0 9 i ci nl o c a lr e a s o n i n g ，p o i n t e ra r i t h m e t i co nd y n a m i ca r r a y s a n dp o i n t e rs e tw i t hl a b e l st ov e r 蚵p r o g r a m si n c l u d i n ga r b i t r a uf u n c t i o n c a l l a sar e s u l t ，p o i n t e rl o g i cc a ng u a r a n t e em o r ep r o g r a m s s a f e t yp r o p e r t i e s t h i st h e s i sd e s i g n se 伍c i e n ta l g o r i t h m sa n dp r o p o s e su n f o l d i n gm e c h a n i s m t oa u t o m a t ep o i n t e rl o 舀cr u l ed e d u c t i o n ，a n da l la r ei m p l e m e n t e di na n a u t o m a t e dv e r i 矗c a t i o nt o o lp l c c ( v 2 ) c o m p a r e dt op l c c ( v 1 ) w h i c h r e q m r e st h ep r o g r a m m e rt op r o v et h ev e r i f i c a t i o nc o n d i t i o n i tg e n e r a t e s ，t h i s 、r ki m p l e m e n t san e w e rv e r s i o nt oa u t o m a t e d l yr e a s o na b o u tt h ep r o p e r - t i e so fp o i n t e rp r o g r a m s m o r e o v e r ，p l c c ( v 2 ) c 龇lv e r i 匆t h eo p e r a t i o n s o nw i d e l yu s e dd a t as t r u c t u r e ss u c ha ss i n g l y l i n k e dl i s t s ，d o u b l y l i n k e dc i r c u l a rl i s t sa n dt r e e se 亡c ，i n c l u d i n gt h ef a m o u ss c h o r r w a i t et r e et r a v e r s a 1 a l g o r i t h mw h i c hi sa l w a y sc o n s i d e r e da st h em i l e s t o n ef o rp o i n t e rf o r m a l i z 舡 t i o n s k e yw b r d s ： s o f 七w a r es a f e t y ， p r o g r a mv e r i f i c a t i o n ， s t o r e l e s sm e m o um o d e l ， i v p o i n t e rl o g i c a b s t r a c t v 中国科学技术大学学位论文原创性和授权使用声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作 所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含 任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本 研究所做的贡献均己在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即： 学校有权按有关规定向国家有关部门或机构送交论文的复印件和电 子版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进 行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论 文。 保密的学位论文在解密后也遵守此规定。 作者签名：玉盍墨 砷年月7 日 绪论 第1 章绪论 在信息时代，计算机软件技术得到了广泛的应用。然而，随着软件功能越 来越强大，软件本身也变得愈发复杂，软件的可靠性和安全性越来越难以得到 保障。无论是在平常的日常生活中，还是在航空航天领域，软件安全也需要得 到越来越多的保障：网上购物的时候我们需要确认银行账号和密码不被非法窃 取；航空航天软件能够确保飞行器在控制的时候不会由于软件漏洞而发生灾 难。因此，软件安全关系到国计民生，软件漏洞不但危害整个系统的安全性， 甚至会导致灾难性的后果。 软件漏洞之所以存在，一方面是软件本身的复杂性导致，而另外一方 面是程序语言的一些特性造成的。在通常使用的c ，c + + 或者j a v a 语言中， 为了使程序能够高效运行，指针或者引用在程序中大量使用。但是指针的 灵活使用很容易引起错误，比如空指针或者悬空指针引用( d a n g l i n gp o i n t e r d e r e f e r e n c e ) ，内存泄露，指向数组的指针还可能引发数组越界访问错误 ( a r r a vo u t o f - b o u n de r r o r ) 。这些错误不仅难以发现，如果一旦发生可能导致 系统崩溃。而且，这些程序漏洞可能被黑客加以利用，比如黑客经常利用缓冲 区溢出来获取系统权限。另一方面，指针错误之所以难以被发现，是因为不同 指针之间存在可能的别名关系( a h a s i n g ) ，即是两个语法上不同的名字在运行 的时候引用同一个内存地址。修改一个名字对应的值，别的名字所对应的值可 能也会随之改变。因而别名信息在决定内存中某个位置是否被修改或者引用至 关重要，但是会给程序调试和程序推理带来很大的困难。因此，带有指针程序 的安全性在软件安全研究中占有重要位置。 在广义上讲：软件安全就是确保软件在运行的时候不出现错误，在工业界 广泛使用软件测试来保障软件不出现错误。然而，虽然软件测试可以发现一些 程序错误，但是通常来说，软件测试并不能或者说难以覆盖程序所能接受的全 部输入，也就是无法发现软件运行时可能出现的所有问题。因而软件测试具有 一定的局限性。对于一些非常关键的软件，比如航空航天类软件，普通的软件 测试已经不能满足其要求。而软件验证给软件危机带来希望，使用形式化方法 可以克服软件测试的这些不足。形式化方法是使用数学逻辑方法来描述程序行 为，因而我们可以用形式化推理来预测程序运行时的行为是否符合特定的规 范，当然也可以包括安全规范。这样在软件开发阶段利用形式化方法就可以发 绪论 现程序运行时可能存在的问题，从而保障交付给客户的软件的安全性。 1 1指针程序验证的相关研究 由于不同的指针之间存在在别名关系，也就是两个语法上不同的名字引 用同一个内存地址，这样就给指针程序的安全性验证带来极大的挑战，也是 当前研究的热点( h i n d ，2 0 0 1 ) 。用于指针程序验证的方法很多，其中包括经典 的h o a r e 逻辑，分离逻辑，基于无存储模型方法，指针逻辑等。除此之外，还有 很多工具被设计来进行指针程序验证。 1 1 1h o a r e 逻辑 使用h o a r e 逻辑进行程序验证早在上世纪6 0 年代就提已经出来( f l o y d ，1 9 6 7 ； h o a r e ，1 9 6 9 ) 。在h o a r e 逻辑中，程序的正确性是由h o a r e 三元组f p s f q 来表 达的，其中s 是程序片段，p 和q 则分别为程序s 的前条件和后条件。前条 件p 描述的是程序s 开始执行时满足的命题，当s 执行完毕，结束状态必须满足 后条件q 。通常，前条件和后条件是由h o a r e 逻辑中的断言语言表达。 h o a r e 逻辑三元组的语法可以由一组形式推理规则表达，其中部分的推理规 则是语法制导的，例如赋值语句规则。也有部分规则是非语法制导的，例如弱 化规则。有了这些规则之后，就可以用h o a r e 逻辑来证明程序的正确性。由于正 确性蕴含了安全性，所以h o a r e 逻辑也可以用来证明程序的安全性。h o a r e 逻辑 使用变量替换来捕获赋值的语义，这样就使得h o a r e 逻辑具有很强的表达能力。 拿赋值语句z ：= e 来说，其中e 为表达式，z 为变量，如果其前条件为磁，则意 味着赋值结束时的状态将满足后条件r 。群表示的是将公式r 中的变量z 的所有 自由出现用e 来替换。注意规则中的z 是简单变量。当用类似的方法来处理含递 归定义数据结构程序时，上述方法将遇到一些困难。第一个困难是由于指针之 间存在别名关系，截然不同的指针之间可能指向同一个对象。第二个困难是断 言中可能还有描述堆结构的归纳定义公式。第三个困难是证明上的：因为不仅 需要形式化的验证集合，序列，图等数据结构，还需要考虑赋值操作对堆影响 的局部性。 当不同的变量名字引用不同的存储空间时，h o a r e 逻辑中的赋值规则是可靠 的。然而，当存在别名时，即当不同的名字描述相同的存储空间，h o a 弛逻辑中 的赋值规则将不再适用。一般来说，别名是由左值( 内存中对象的地址) 的重 叠引起的，但是令人欣慰的是，指针别名判断可以用比较右值( 内存空间中的 内容) 来实现。而h o a r e 逻辑规则中全部都是处理右值的。因此，用h o a r e 逻辑 2 绪论 来证明指针程序的正确性是可行的。 实际上，计算机中的内存是一个巨大的数组，而内存地址，即通常所说的 左值或者指针，其实就是它的索引。任何时候只要两个指针的值是相等的，指 针别名现象就出现了。因此，可以将整个堆看成是一个指针作为索引的数组， 数组中的每个元素都是以部件作为索引的对象。同时，将对象类型再分成子数 组类型( l e i n o ，1 9 9 5 ；l u c k h a ma n ds u z u l 【i ，1 9 7 9 ) 。但是这种方法具有不可操作 性。首先需要设计程序中的对象部件公式和数组索引公式之间的一种翻译机 制。其次，它使得推理必须是全局的：每个对象部件的赋值都要与整个堆联系 在一起。其实在h o a r e 逻辑中，赋值语句规则只处理含有要赋值变量部分，而保 持其他部分不动。最后，关于堆内容的断言通常需要归纳项表达，而辅助的归 纳定义会比较容易的隐藏指针之间的别名关系。然而，这些困难都是可以克服 的，问题是程序员编程的时候不会总想着内存是一个大数组，丽是认为处理的 是不同的变量，数组，对象等。 因此，h o a r e 逻辑比较少的用于指针程序的验证，但是研究就一直没有停 止过。早在7 2 年，b u r s t a u 就在论文中给出处理链表的方法( b u r s t a u ，1 9 7 2 ) ， 指出在对象部件( o b j e c tc o m p o n e n t s ) 和数组元素之间存在相似性。到 了1 9 8 1 年，m o r r i s 提出给对象部件赋值的公理来描述处理归纳定义数据结构的 机制( m o r r i s ，1 9 8 1 ) ，并给出s c h o h - w a i t e 图标记算法( s c h o r ra n dw a i t e ，1 9 6 7 ) 的 半形式化证明( s e m i f o r m a lp r o o f ) 。 m o r r i s 设计了一种类似于j a 的语言：支持指针别名，不支持参数别名 ( p a r a i n e 乇e r - a l i a s i n g ) 和对象整体赋值。在这个假设下，栈变量例如z ，爹，ng 可 以是指向堆中对象的指针。堆中的对象具有索引为e ，夕， 之类的部件( 域) ， 而且可以通过后缀点标记引用域，例如p e e 厂。在这些前提下，别名只存 在对象的域之间。因为在对象域的名字不会参与运算，因此只要域e 与，的 名字不同，不管对象a 与b 的值是什么，a e 与b ，的左值不可能相同。同 样，a 与b e 的左值一样当且仅当a 与b 的右值相等。对象域之间的左值别 名关系因而可以比较对象域的名字和指针的右值得到。赋值语句的规则如下： 毒 ( 1 1 ) _ 【q ) a ，：= e 【冗 、 对象域替换磋，几乎和变量替换一样，除了它需要处理对象域的引用之 外。m o r r i s 的公理如下： 车g ( b 9 ) 2 ，圭b 9 ( 1 2 ) 3 绪论 其中三表示是语法相等。 ( 曰厂) 鲁，三i fa =bt h e nee i s e8 ，厂f i ( 1 3 ) 但是，m o r r i s 的方法具有局限性一它只能处理对象域的名字只出现一次的情 况，例如可以正确的处理p d 和p t f 但却不能正确处理p 九d f 。 除此之外，还有很多学者在h o a r e 逻辑里面嵌入内存模型到断言逻辑 中来保证指针程序的正确性。例如l u c k h a m 和s u z u k “l u c k h a ma n ds u z u k i 1 9 7 9 ) ，l e i n o ( l e i n o ，1 9 9 5 ) 和b 巧l s m a ( b i j l s m a ，1 9 8 9 ) 等，使用指针类型来标记堆 的各个部分。 其他的工作也意识到数组元素和对象部件之闻i 的相似性，但是没有进行有 效的处理咭例如，h o a r e 和w i r t h ( h o a r e ，1 9 7 4 ) 与g r 洒和l e v i n e ( g r i e sa n dl e v i i l ， 1 9 8 0 ) 只给出了处理最简单非指针情况的对象部件赋值公理，完全忽路处理指针 别名时的情形。 c h a r db o r n a t 则注意到：由于堆中的对象不会重叠，整个堆可以看成是由 指针索引的对象组成，而每个对象又是由名字索引的域组成( b o r n a t ，2 0 0 0 b ) 。 因而，堆日中对象域a 厂的引用就可以对应一个双引用，一次是堆上的，一次是 对象上的。对于赋值a ，= e ，与夕不同，则有： ( b 9 ) 叁。，之( b 会。，) 9 ( b ，) 会，圭i fa = j e i 鲁，t h e nee l s e ( j e 7 会，) ，f i ( 1 4 ) ( 1 。5 ) 按照上面的思想，对对象a 域，的赋值可以看成是对以a 为索引的域分量数 组，访问a ，就如同访问域分量数组，的第a 个元素。将域作为数组方法的好处 很多；首先，可以用它来计算最弱前条件；其次，这意昧着可以不用新的结构 化归纳方法处理对象分量替换一证明和证明检查将会变得相对容易。最后，也 是最重要的是，对象域替换的形式化处理变成了归纳结构公式。 在这个思想的指导下，b o r n a t 利用交互式定理证明 器j a p e ( b o r n a ta n ds u f r i n ，1 9 9 9 ) 证明 了s c h o r r w 撕t e 图标记算 法( s c h o r ra n dw 缸t e ，1 9 6 7 ) 的部分正确性。然而，j a p e 只是一个几乎没有 自动化功能的证明编辑器，这导致整个证明花了1 5 2 页( b o r n a t ，2 0 0 0 a ) 。并 且，b o m a t 的逻辑基础不是很牢固：他需要处理的链表可能是潜在无限的或者 是没有定义的，但是又显式地忽略了确定性。 4 绪论 f a r h a dm e c h t a 和t o b i a sn i p k o w 沿用b o r n a t 提出的思想，将堆看成从地址到 值的映射，而指针结构则映射到更高层的数据结构，然后在h o a r e 逻辑中进行程 序推理( m e h t aa n dn i p k o w ，2 0 0 5 ) 。他们研究了如何将验证指针程序的h o a r e 逻 辑嵌入通用定理证明器中，并提出一种在指针层面上验证归纳定义数据类型例 如链表与树的逻辑可靠的方法。比b o r n a t 的工作更进一步的是，他们不仅在定 理证明器i s a b e l l e h o l ( n i p k o we ta 1 ，2 0 0 2 ) 中再次证明了s c h o r r - w 批e 图标记算 法的部分正确性，而且生成了一份可以人工阅读以及可以被机器检查的证明。 1 1 2 分离逻辑 b u r s t a l l f b u r s t a l l ，1 9 7 2 ) 关键思想是将堆看成。砌r e s s t ，口z 缸e 的变量类型 集合。而由r e y n o l d s 和p e t e ro h e a r n 等提出的分离逻辑就是在此基础上发展 的h o a r e 逻辑扩展，可以对共享易变性数据结构( s h a r e di n u t a b l ed a t as t m c t u r e s ) 进行推理( o h e a r ne ta 1 ，2 0 0 1 ；r e y n o l d s ，2 0 0 2 ) 。共享易变数据结构，从 名称上来看即是一种可被更新的域可能从多个点引用的结构，因而在各种系统 实现和人工智能中得到了广泛使用。虽然关于这方面的研究非常多，但是要么 应用有限，要么异常复杂以至于不能应用到一般大小的程序上。这些方法所面 临的问题就是：改变数据结构的程序正确性通常取决于对这些结构共享的异常 复杂的限制。 避免这种困难出现的关键是创新性地引入分离析取逻辑操 作p 木q ，其中断言p 和q 分别在存储空间不同部分成立。分离析取 的主要概念在b u r s t a l l 的早期思想“相异不重复树系统隐式的提 到。9 9 年秋，r e y n o l d s 显式的描述了这个概念，并将其嵌入到h o a r e 逻 辑( h o a r e ，1 9 6 9 ，1 9 7 1 b ) 中。很快，i s h t i a q 和o h e a r n ( i s h t i a qa n do h e a m ，2 0 0 1 ) 和r e y n 0 1 d s ( r e y n o l d s ，2 0 0 0 ) 独立发现基于上述思想的一种直觉逻辑。在意识到 分离逻辑就是强蕴含( b u i l c h e di m p l i c a t i o 璐) ( o h e a r na n dp y m ，1 9 9 9 ；p y m ， 2 0 0 2 ) 逻辑的一个实例之后，i s h t i a u q 和o h e a r n 引入了分离蕴含p 一章q 。 具体的来讲，在分离逻辑中，程序规范以h o a r e 三元组形式出现， 即： q 1 cf p l 。除此之外，还有一个表示程序堆和栈的状态。因而从本 质上来说，分离逻辑是谓词演算的扩展： 空堆：断言e 唧成立当且仅当堆中不含有内存单元。 单件堆( s i n g l e t o nh e a p ) ：断言xhe 成立，当且仅当堆中只有一个存 储单元，即在地址x 的内存单元的内容为e 。 分离析取：断言尸奉q 对堆日成立当且仅当堆日可以被分为两个不相交的子 堆凰和仍，其中p 在子堆玩成立，q 在子堆凰中同时成立。 5 绪论 分离蕴含：断言p _ 聿q 成立当且仅当当前堆凰能被一个能使断言尸成立的 不相交的堆飓扩展，q 在扩展之后的堆中成立。 注意xhe 形式的断言只描述单件堆，而分离析取可以描述任何大小的堆。 分离逻辑中最核心的证明规则是框架规则( f r a m er u l e ) ( o h e a r ne ta l l ， 2 0 0 1 ；1 r a n ga n d0 1 h e a r n ，2 0 0 2 ) ： p ) c q ) 尸宰兄) c q 牢兄】 ( 1 6 ) 其中程序c 没有改变断言冗中的任何自由变量。使用框架规则就可以扩展仅仅包 括程序g 使用的变量和部分堆( 称为c 的封装) 的局部规范：可以加入关于不被 程序c 所改变或更新的变量或堆的任意命题。因而，框架规则是局部推理的关 键：为了理解一个程序如何工作，推理和规范都应该限制为程序实际访问的存 储单元。其余的任何其他存储单元应该自动的保持不变。 因此，每个正确的规范 p _ c q ) 是紧致的，也就是在某种程度上程序c 的 封装里面的每个存储单元或者是由c 分配的，或者是断言p 声称是活性的。而局 部性就是其逆命题：每个存储单元如果断言为活性，则它一定属于封装。框架 规则的任务就是从命令( c o m m a n d ) 的局部规范推导出适应全局规范的更大的 命令封装。注意框架规则里面的附加条件，即r 中没有任何自由变量被c 改变。 正是框架规则支持了局部推理，也就是说为了证明c 的正确性，框架规则允许 研究者只关注和c 有关的变量和部分堆。 分离逻辑的直觉特性蕴含了其单调性：如果一个断言在某部分存储地址空 间内成立，则对于这部分空间之外的任何扩展，例如内存分配，断言仍然会成 立。 分离逻辑具有很强的表达能力，并且能够通过分离析取获得局部推 理能力，因而很适合于验证动态分配的链式数据结构，同时也获得比以 前形式化方法简单很多的手工书写规范和程序证明。近年来，使用分离 逻辑验证指针程序的研究很多，而关于指针程序自动化的研究要相对少 一些。b e r d i n e ，c a l c a g n o 和0 1 h e a r n 设计了一个工具s m a l l f o o t ( b e r d i n ee ta 1 j 2 0 0 5 a 1 。他们的目的是为了查看使得分离逻辑中的手工证明的简单性能否被 自动化的实现。s m “l f o o t 使用轻量级的断言，即只描述数据结构的形状而非其 中的内容，这样推理就可以完全自动化。输入语言允许带有引用和传值参数 的过程，和文献( h o a r e ，1 9 7 1 a ) 设置样，同时支持内存分配、释放、修改和 读写，并要求过程具有前条件，后条件和循环不变式。s m a l l f o o t 靠符号执行 ( s y n 幽o l i ce x e c u t i o n ) ( b e r d i n ee t “，2 0 0 5 b ) 来发现程序证明。在s m a l l f o o t 所 6 绪论 支持的断言都具有形式八，是一个由 组成纯布尔条件，而是由水组合 的堆谓词。堆谓词包括指向关系，树谓词，一个单向链表段谓词和异或链表 谓词。这样做的好处是利用符号执行机制，而由木联结的谓词可以原地被更 新。s m a l l f