【www.rjdtv.com--工程论文】

　　1、引 言

　　在信息技术高度发展今天，日常生活以及各行各业的生产已经无法离开软件系统． 因此软件的安全性与可靠性也就深深的影响到社会的发展． 软件安全的研究为国家安全稳定与经济社会的持续健康发展提供有力的保障． 保障软件安全可靠的方式有很多种，其中之一便是利用形式化验证的方式来提高软件可信度． 概括来说，形式化验证有两种方式: 第一是模型检测，通过遍历系统所有的状态空间，能够自动验证有穷状态的系统并构造不满足性质定理的反例; 第二是逻辑推理，程序员需要提供断言语言来描述程序需要验证的性质，然后使用某种推理规则( 如 Hoare 逻辑［1］，分离逻辑［2］等) 来对程序进行逐步分析和推理生成验算结果，并依靠 Z3［3］等定理证明器进行辅助证明这些演算结果．我们课题组基于第二种方式实现了一种自动化的面向安全 C 语言的程序验证系统，其中程序员提供的断言语言是基于 SCSL( Safe C Specification Language) 语言( 参考 ACSL［4］设计) ，推理规则是基于 Hoare 逻辑规则上的扩充． 在实现系统过程中，我们发现使用基于 Hoare 逻辑的程序断言仅表示程序变量在某一个程序状态下的性质，在程序状态改变时，程序断言将无法描述状态改变前后程序变量值之间的联系，而保存这种前后状态的联系对于验证系统是必要的． 我们的解决方法是在程序断言中引入逻辑变量，例如:

　　1) 对任何 x，若 x 大于变量 m，则经过赋值语句 m = m-1后，x 大于 m +1．2) 对于任何 y，若 y 大于二叉排序树 t 上的所有数据，并且 y 大于插入数据 data，则 y 大于结果二叉排序树上的所有数据．本文贡献在于通过在断言语言中引入逻辑变量，解决了断言语言无法记录程序上下文性质的缺点，同时也探讨了引入断言语言带来的问题并给出了一个可行的解决方式．

　　2、验证系统介绍

　　我们开发的验证系统分为三个部分: 第一部分为程序分析模块，负责分析程序代码和断言语言; 第二部分为形状图模块［5］，负责生成各个程序点的形状图; 第三个部分为验证模块，依据各程序点的断言和形状图进行演算，并生成验证条件交由 Z3 证明． 以下分为两节，第一节简单介绍三个部分涉及理论基础，第二节介绍验证系统框架．

　　2． 1、程序分析与形状图

验证系统是用来验证由 C 语言开发的程序，为此我们设计了 SCSL 用来描述程序行为性质，并对 Hoare 逻辑的推理规则进行了必要扩展． 针对含指针程序难以验证这一特点，我们则设计了形状图逻辑［5，6］．

　　其中 G 表示形状图，它是程序中与指针相关的断言的图形表示． Q 描述除指针以外程序变量相关的断言． S 是程序片段． 程序点完整断言便是 G∧Q． 在演算过程中，由于 G 并不受 Q 影响，因此形状图模块程序规范可简化，然后利用形状图推理规则独立演算生成各个程序点的形状图． 并最终交给验证模块．

　　2． 2、验证系统框架

　　验证系统框架如图 1 所示，整个验证流程是: SCSL 描述的 C 语言源程序经过前端( 基于 clang［7］二次开发，使之能够分析 SCSL) 生成 C 程序和 SCSL 断言的抽象语法树，并使二者相关联． 然后进入形状图模块，推导生成各个程序点的形状图，while 等循环语句的循环不变形状图［5，6］( 循环中指针 不 变 性质) 等，并与程序抽象语法树关联，为第三部分验证条件生成器提供别名判断等支持． 最后验证条件生成器依据 Hoare 逻辑推理规则，扫描程序抽象语法树，SCSL 断言以及形状图进行演算生成验证条件． 最后对验证条件进行适当转换，交给 Z3 进行证明并输出证明结果．图1 中形状图系统不仅仅给验证条件生成器提供指针别名信息，因为在各个程序点，仅仅将当前程序点得到的验证条件 Q 交给 Z3 证明，可能会因为 Q 中没有指针相关断言而无法证明．

　　转换成 Z3 接受的形式交给 Z3 证明．我们课题组当前实现的验证系统与一个先前的验证系统原型［8，9］的区别有两点: 1) 先前的验证系统是用来验证类似C 语言的小型语言 PointerC 编写的程序( 详细文法见［6］) ，而当前验证系统则是面向验证安全 C 语言编写的程序; 2) 先前的系统并未使用 SCSL 语言描述程序行为性质，而是将描述语言直接集成在 PointerC 文法中，其描述能力也十分有限．

　　3、问题描述与解决方案

　　3． 1、Hoare 逻辑介绍

　　Hoare 逻辑是形式化验证领域重要程序逻辑之一，其核心是 Hoare 三元组，三元组描述程序的执行是如何改变计算状态． Hoare 三元组形式为{ P} C{ Q} ．其中 P，Q 是断言，C 是程序． P 是前条件，Q 是后条件．在 Hoare 三元组中，断言 P，Q 表达程序变量在某个程序状态的性质． Hoare 三元组在直观上可用语言描述为: 只要 P在 C 执行之前的状态下成立，则在 C 执行之后 Q 成立．在 Hoare 逻辑中，程序断言 P，Q 表达程序变量在某个程序状态下的性质，难以描述程序变量在不同状态下的值之间的联系． 例如赋值语句 m = m +2 的 Hoare 三元组表示形式为{ m =0} m = m +2{ m =2} ( 假设 m 初始值为 0) ．以上形式无法表达 m 在赋值之后比赋值之前值增加 2．一种简单的解决办法是使用本文介绍的逻辑变量． 若使用逻辑变量 oldm 记录 m 赋值之前的状态，则以上 Hoare 三元组可写成为{ oldm == m} m = m +2{ oldm == m －2} ．以上形式便很好的体现出了 m 赋值后与赋值前值的关系．

　　3． 2、引入逻辑变量的作用

　　逻辑变量的主要作用是记录程序上下文中的一些性质，以下是逻辑变量的两种典型应用．逻辑变量的一种典型应用是表达函数参数在函数返回点具有的性质． 对于在函数体中可对形参赋值的语言，一般禁止形参出现在函数后条件中． 这是因为形参可能被重新赋值，形参在函数返回点具有的性质不能作为实参在调用点之后的性质． 这里以复制单向链表的函数 listcopy( Node* p) { …; re-turn q; } 为例，其代码如下页图 2 所示，解释函数前后条件{ sortedlist( p) oldp == p} 和{ sortedlist( q) ∧ sortedlist( oldp) }中逻辑变量 oldp 的作用． 图中出现在”/* @ …* /”中的便是SCSL 书写的程序断言． 其中 requires，ensures 是分别用来描述函数的前后条件的关键词，其后的断言便是函数前后条件．sortedlist( p) 是自定义谓词［9］，是有序单链表的归纳定义，其定义可以解释为:

　　1) 若节点 p 为空，则 p 指向有序单链表．2) 或者 p 指向单节点则 p 指向有序单链表．3) 否则 p、p→next 不为空，且 p→next 有序同时 p→data＜ p→next→data，则 p 指向有序单链表．若某次调用的实参是 t，它具有性质 sortedlist( t) ． 把函数前条件中的形参 p 代换成实参 t，再把函数前后条件中的逻辑变量 oldp 也代换成 t，则调用点的断言蕴涵前条件 sortedlist( t) ∧t == t，因而调用后有断言 sortedlist( q) ∧sortedlist( t) ，即实参 t 在调用之后仍然指向有序单链表．

　　4、证明实例

　　下面通过一个证明实例来简述断言语言中引入逻辑变量后的验证，本例是向平衡二叉树中插入新节点的递归实现，详细代码、断言以及逻辑定义见图 3．函数前后条件中的 y ＞ data ＆＆ gt( y，p) 和 gt( y，/result)表示的意思是: 对于任何值，只要在调用前它大于被插入数据data 并且大于 p 所指向二叉树上的所有数据，则它也大于插入 data 后的结果二叉树上的所有数据．近年来有关程序验证的一些研究工作［12-14］都使用逻辑变量来描述程序规范，但它们都没有像本文这样系统地讨论逻辑变量的使用和实现技术．

（参考文献：略）

本文来源：http://www.rjdtv.com/gongchenglunwen/2572.html