| 本文已被：浏览 5325次 下载 6305次 |
码上扫一扫！ |
|
|
| 基于Assume-Guarantee搜索复用的C程序验证方法 |
|
易晓东1, 王戟1,2, 杨学军1,2
|
|
1.国防科学技术大学,计算机学院,湖南,长沙,410073;2.并行与分布处理国防科技重点实验室,湖南,长沙,410073
|
|
| 摘要: |
| 提出了一种基于Assume-Guarantee搜索复用的验证方法,对C程序源代码进行验证.其思想是,在程序的每点处都引入一个保守假设条件,并假设从任意点出发,变量取值满足该点假设条件的所有执行路径都不会违背给定性质,然后根据这些假设条件遍历所有可能的执行路径以验证给定的时序安全性质,并在遍历的过程中验证这些假设条件是否满足,如果不满足,则不断对其精化和加强.验证方法总是在保证假设条件可靠的前提下尽量使用较弱的条件,使得大量的执行路径由于满足假设条件而可以搜索复用,从而降低验证代价.应用该方法验证了Linux操作系统中SSL协议的实现程序openssl-0.9.6c满足SSL协议的初始握手规范.实验结果表明,该方法具有良好的实用性和可扩展性. |
| 关键词: Assume-Guarantee搜索重用 变量抽象 程序近似语义 部分最强后置条件 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant No.60233020 (国家自然科学基金); the National High-Tech Ressearch and Development Plan of China under Grant No.2006AA01Z429 (国家高技术研究发展计划(863)); the Program for New Century Excellent Talents in University under Grant No.NCET-04-0996 (新世纪优秀人才支持计划) |
|
| Verification of C Programs Using Assume-Guarantee Reuse of Searching |
|
YI Xiao-Dong,WANG Ji,YANG Xue-Jun
|
| Abstract: |
| This paper presents a novel method,namely Assume-Guarantee reuse of searching,to verify C programs with respect to temporal safety properties.Its idea is to introduce a conservative assume condition for each program location,and to assume that every path starting from the program location will never violate the property if the evaluation of its variables at that location satisfy the assume condition.All the possible execution paths are traversed based on the assume conditions,and the temporal safety property is checked on the fly.If some assume condition is too weak,it will be continually strengthened based on the spurious counterexamples.The presented verification method can try to adopt the weak assume conditions so as to let more execution paths satisfy the conditions and to reuse the searching efforts.Therefore,a significant reduction of verification cost can be achieved.The verification method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c.The experimental results demonstrate that the method is both effective and practical. |
| Key words: Assume-Guarantee reuse of searching variable abstraction approximated program semantics partial strongest post-condition |
