论文部分内容阅读
软件验证作为保证软件正确性,提高软件可靠性的关键技术,受到了大量关注和广泛研究。循环不变式在软件验证领域发挥着不可替代的作用,它不仅是传统的归纳断言法的基石,也在目前流行的很多软件验证相关的技术中扮演着重要的角色。然而,循环不变式的自动构造技术一直是一个巨大的挑战。本文对面向程序验证的循环不变式自动构造相关理论和算法进行了系统、深入的研究,主要工作包括以下五个方面:1.提出一个多路径循环多项式等式循环不变式构造算法,并证明了算法的正确性,给出了算法的终止性条件。该算法保留了基于Gro¨bner基方法的循环不变式构造算法的高效性;采用控制流精化技术,识别循环中路径交叠的结构,从而构造与路径条件相关的循环不变式;能够构造析取形式的循环不变式。2.基于表达式的有限差分,提出一个迭代的多项式等式循环不变式构造算法,并证明了算法的正确性。该算法基于参数化模板和约束求解技术,采用迭代的方式,借助次数较低的(甚至平凡的)多项式等式不变式,逐步构造次数较高的多项式等式不变式。经典的基于约束求解的循环不变式构造算法需要求解非线性的等式约束,而我们的算法仅需要求解线性的等式约束。3.针对变量值域为有限数域的程序,提出了一种基于QBF的循环不变式构造方法。该方法采用参数化的循环不变式模板,将程序转化为约束,并使用QBF求解器对约束求解,从而得到循环不变式。该方法允许程序中包含非线性的表达式,支持复杂的算术和逻辑运算,包括乘、除、位操作和移位等,能够构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,以及包含量词的不变式。采用该方法构造的循环不变式与程序的实际执行吻合。4.设计实现了一个基于QBF的循环不变式构造工具。工具以CIL作为前端,以C语言程序作为输入,可以自动地构造循环的不变式。5.设计并实现了一个C语言缓冲区溢出漏洞的有效检测工具CBOC。该工具基于符号执行,并引入基址安全表达式的概念,优化了符号执行过程。CBOC以CIL作为前端,以C程序源代码作为输入,能自动检测出程序中包含的缓冲区溢出漏洞。