反例引导的C代码空间流模型检测方法

Counterexample-guided Spatial Flow Model Checking Methods for C Codes

软件验证一直是确保软件正确性和安全性的热点研究问题.然而,由于程序语言复杂的语法语义特性,应用形式化方法验证程序的正确性存在准确度低和效率差的问题.其中,由指针操作带来的地址空间的状态变化使得现有模型检测方法的检测准确度难以得到保证.为此,通过结合模型检测与稀疏值流分析方法,设计了一种空间流模型,实现了对C程序在符号变量层面和地址空间层面的状态行为的有效描述,并提出了一种反例引导的抽象细化和稀疏值流强更新算法(CEGAS),实现了C程序指向信息敏感的形式化验证.建立了包含多种指针操作的C代码基准库,并基于该基准库进行了对比实验.实验结果表明:所提出的模型检测算法CEGAS在分析含有多种C代码特性的任务中,与现有模型检测工具相比均能取得突出的结果,其检测准确度为92.9%,每行代码的平均检测时间为2.58 ms,优于现有检测工具.

Software verification has always been a hot research topic to ensure the correctness and security of software. However, due to the complex semantics and syntax of programming language, applying formal methods to verify the correctness of programs has the problems of low accuracy and low efficiency. Among them, the state change of address space caused by pointer operations makes the verification accuracy of existing model checking methods difficult to be guaranteed. By combining model checking and sparse value-flow analysis, this study designs a spatial flow model to effectively describe the state behavior of C codes at the symbolic variable level and address space level, and proposes a model checking algorithm of counterexample-guided abstraction refinement and sparse value flow strong update(CEGAS), which enables points-to-sensitive formal verification for C codes. This study establishes a C code benchmark containing a variety of pointer operationsand conducts comparative experiments based on this benchmark. These experiments indicate that in the task of analyzing multi-class C code features, the model checking algorithm CEGAS proposed in this study can achieve outstanding results compared with the existing model detection tools. The verification accuracy of CEGAS is 92.9%, and the average verification time of each line of code is 2.58 ms, which are both better than existing testing tools.