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

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