基于Assume-Guarantee搜索复用的C程序验证方法

Verification of C Programs Using Assume-Guarantee Reuse of Searching

提出了一种基于Assume-Guarantee搜索复用的验证方法,对C程序源代码进行验证.其思想是,在程序的每点处都引入一个保守假设条件,并假设从任意点出发,变量取值满足该点假设条件的所有执行路径都不会违背给定性质,然后根据这些假设条件遍历所有可能的执行路径以验证给定的时序安全性质,并在遍历的过程中验证这些假设条件是否满足,如果不满足,则不断对其精化和加强.验证方法总是在保证假设条件可靠的前提下尽量使用较弱的条件,使得大量的执行路径由于满足假设条件而可以搜索复用,从而降低验证代价.应用该方法验证了Linux操作系统中SSL协议的实现程序openssl-0.9.6c满足SSL协议的初始握手规范.实验结果表明,该方法具有良好的实用性和可扩展性.

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.