这次我们要探讨的问题是,CBMC的架构是什么,并且是如何将程序转换成公式的。我们通过 Daniel 给的 CBMC V1.0的介绍(slides),加深对初始 CBMC 架构的理解。

Now, let us look inside CBMC and figure out how cbmc works and how does it generate VC. We first download the slides explaining the first version (v1.0) of cbmc given by Daniel. That will help us understand cbmc’s structure.

cbmc

前端处理 frontend

frontend of cbmc

cbmc 的目标是分析 C/C++ 或者 JAVA 程序。CBMC 的第一步是输入程序,生成 CFG。关于如何生成 CFG,是编译原理的基础课程(我们可以用 CIL 来初步处理程序获得 CFG,另外,frama-c 平台也提供了现成的模块,可以直接获取)。

cbmc aims at the analysis of programs given in a commodity
programming language such as C, C++, or Java As the first step, it transforms the program into a control flow graph (CFG)

cfg example

当我们获取程序的 cfg 图时,我们就可以获取每条路径 pip_{i} 对应的公式 ϕi\phi_{i},也就是说,路径pip_{i} 能够执行的条件是ϕi\phi_{i} 能够成立。

When we have the cfg, that means we have the execution paths of the programs. Thus, we can obtain the conjunction (ϕi\phi_{i}) of the condition in each joint point for each path ϕi\phi_{i}. The path will be executed if ϕi\phi_{i} is valid.

我们选择其中的一条路径,这条路径对应的逻辑公式。获取公式之后,我们需要找到判定过程( decision procedure),获得公式的解。

let us look at the example in the above graph. We select one path and obtain the corresponding formula. This formula should be passed to a decision procedure and we obtain a satisfying assignment or the formula is invalid.

对于不同类型的公式,我们需要不同的判定过程。对于判定过程的介绍,可以阅读 Daniel 的《判定过程》一书,其中介绍了 propositional/predicate logic、array、pointer等不同逻辑的判定过程。很多 SMT 已经提供很多判定过程。比如 Z3, Yices等等。

SAT

最简单和初步的就是 SAT,是针对解决命题逻辑的。

SAT 的求解技术能力已经有了明显的提升。目前的很多研究是提高 word-level reasoningarray decision procedures 的效率。

另外,我们也可以看出,有些公式是无解的,比如下图中的例子。

SSA

针对不同类型的程序,我们需要适当做变换,使得公式生成得更简单。更为复杂的例子是,假如我们处理循环,循环中的变量会一直变,比如以下的例子:

针对这样的程序,我们可以通过重命名,获得SSA (static single assignment)。

pointer

另外一个复杂的例子是,如果程序中有指针和引用呢?

pointer

针对引用,我们引入抽象值(abstract state)来表示指针可能指向的地址。对于指针 p,我们假设其是指向 DO1DO1 的 的地址。

处理循环

针对不能终止的循环,cbmc 的策略是给定一个深度(only look for bugs up to specific depth)。

Transition System

A transition system (S,T,I)(S, T, I) is defined as follows:

  • a set of states SS;
  • a transition relation T:SST: S \rightarrow S;
  • a set of initial states S0SS_{0}\subseteq S.

A program is modelled as a transition system. Each state of the program is an evaluation of all variables in the program. Each state may has many possible successors, i.e., the transition relation is non-deterministic.

Example1 : S={a,b,c}S = \{a,b,c\}, I={a}I = \{a\} and T={a,b,b,b,b,c}T = \{ \langle a,b\rangle, \langle b,b\rangle, \langle b,c\rangle\}

Q: How do we avoid the exponential path explosion?

上述公式对应着 TS 中的路径。在下面的例子中,转移函数只有一个,TS 的初始条件也给出。我们可以得到深度为 4 的公式。

Reachability

如果想要检查可达性,比如我们想要验证,在所有的 TS 状态中,至少有一个状态 SiS_i 满足 ¬p\neg p。我们就可以提到相应的性质公式:

在下面的例子中,我们可以对程序的 cfg 展开 6 次。

example 1

example 2

对于一个 TS 系统 TT, 设定展开的界限是kk,那么我们就能得到大小为 Tk|T|\cdot k 的公式。slides 上说,如果 kk 是线性的,那么得到的公式大小就是 O(T2)O(|T|^{2}) (但是我不知道为什么?)

Unroll loop

对于循环,是否有更好的方式呢?

目前为止,我们已经搞清楚了 cbmc 怎么将程序生成公式,在生成的过程中,也有很多策略可以使用。

总结

cbmc 的步骤总共有三步:

  1. 前端处理,获得程序的 cfg
  2. 展开 unwind cfg,获得路径的公式
  3. 利用 SAT/SMT 求解公式

其中,2,3两步是重点。