ESBMC-An Efficient SMT-based Software Model Checker

1. Introduction

It(ESBMC) does not require any special annotations in the source code to find such bugs, but it allows users to add their assertions and checks if they hold. In addition, ESBMC implements a k-induction proof rule and can be used to prove the absence of property violations (resp. the validity of user-defined assertions)

  • 它（ESBMC）不需要在源代码中进行任何特殊的注释来发现这种错误，但它允许用户添加他们的断言并检查它们是否成立。此外，ESBMC实现了一个k-归纳证明规则，可以用来证明没有违反属性（即用户定义的断言的有效性）

2. ESBMC Architecture

  • One of the significant challenges in software verification is the development and maintenance of an infrastructure that can reliably and efficiently handle real-world programs; it is an issue that only intensifies given the ever-evolving programming language standards.
    • 新标准发布需要新的支持

2.1. Front-end

  • an important piece of technology that should facilitate the transition between the program under verification and a format the tool can work upon

2.1.1. Clang

Clang是LLVM编译器的c-family前端，Clang可能意指三种不同的实体：

  • 前端（在Clang库中实现）
  • 编译器驱动程序（在clang命令和Clang驱动程序库中实现）
  • 实际的编译器（在clang -cc1命令中实现）。clang -cc1中的编译器不仅是由Clang库实现，还广泛地使用其他LLVM库来实现编译器的中端、后端以及集成的汇编器。
  • clang -emit-llvm -c size.c -o size.bc

Using the LLVM bitcode in the verification process brings some advantages; the bitcode is highly optimized by LLVM and will simplify the verification, thus reducing costs. However, there are disadvantages to this process, including losing context information (e.g., variable, class and function names are mangled in C++ ), source location information; in rare cases, optimizations can generate wrong results . While the latter can be avoided by disabling optimizations (and thus losing one of this approach’s advantages), the other two are not easily avoided by software verifiers.

  • 其他前端的不足还是在于会丢失source location information
    • 丢失了会怎么样呢？

2.1.2. ESBMC Front-end

  • Instead of working on the LLVM bitcode, ESBMC accesses the AST that generates the bitcode
    • We developed a new front-end based on clang.
    • We use clang to parse the C program, which generates the clang AST, and we convert it to the ESBMC AST

2.1.3. versus

  • The clang front-end brings several advantages to the verification process.
    • First, clang has a powerful static analyzer. It can provide state-of-the-art compiler diagnostics of the program, thus issuing the same warnings and errors that one would expect from a conventional compilation.
    • Second, the support for new language features is simplified. A newAST node converter needs only to be added to the converter class in ESBMC, rather than layering in the feature from flex lexer to type-checker.
    • Finally, by choosing the AST instead of the bitcode, a complete representation of the original program is available, including the original names of every class, function, and variable.
  • The disadvantage is that ESBMC is unable to access the optimizations that LLVM performs on the bitcode

2.2. GOTO Converter

  • This representation is similar to the control flow graph (CFG) representation used by conventional compilers, but we associate program statements with edges.

    • In this process, the GOTOprogram is also simplified, and new property checks and instructions can be added.

  • The GOTOprogram is a simplified version ofthe program: a branch and a backward GOTO replace for and while loops. It is very similar to a C program, containing assignments, function calls and returns, and location information.

  • Once the GOTO program is generated, the following transformations can be applied, depending on the set of options given to ESBMC:

    • Function inlining
      • replaces function calls with the instructions of the called function.
    • Interval analysis
      • performs an interval analysis区间分析 for integer variables
      • The intervals are added back into the GOTO program as assumptions
    • Code transformations
      • introduce new instructions depending on several factors.
      • In particular, concurrency instructions can be inserted if the program is multi-threaded, and k-induction specific instructions are introduced if kinduction verification is enabled
    • Property checks
      • can insert several property checks into the GOTO program, including division by zero checks, integer, and float overflow checks, NaN checks (i.e., whether the result of an operation can be NaN), data race checks, deadlock checks, and atomicity checks. All these properties are encoded as assertions in the GOTO program.

2.3. Symbolic Engine: Generating SSA

static single assignment (SSA)

  • unwinds解开 the GOTO program from the previous step

  • add further property checks, including dynamic memory checks (bounds, memory alignment, offset pointer-free, and double-free) and unwinding assertions

  • Main Goal: introduce fresh copy for each occurrence

…

2.4. SMT Solver: SMT Encoding of C Programs

After the SSA set is created, the next step is to encode every (not sliced) assignment in SMT and check for satisfiability.

  • We use a notation of constraints C and properties P when encoding the set of SSA.
    • A constraint is an assignment or an assumption in the program. It constrains the value of a variable
    • while a property is an assertion in the program. This property needs to hold given the set of constraints.
  • The constraints and properties are encoded in the form $C∧¬P$: given the set of constraints, the SMT solver will try to find an assignment to variables that satisfies the constraints and violates at least one property.
    • SMT求解器将试图找到一个满足约束条件并至少违反一个属性的变量赋值
  • Finally, if the SMT solver finds a model, ESBMC will generate a program counterexample: a set of assignments and the program’s violated property.

…

3. ESBMC’s Verification Modes

3.1. Bounded Model Checking

  • Bounded Model Checking | 烏巢

  • A node in the CFG represents either a (non-) deterministic assignment or a conditional statement, while an edge in the CFG represents a possible change in the program’s control location.

    • CFG中的一个节点代表一个（非）确定性的赋值或一个条件语句，而CFG中的一条边代表程序控制位置的可能变化。

  • This graph is built as part of a translation process from program text to SSA.

  • A state transition system, denoted by M, is defined by a triple $(S, R, s_1)$ where S represents the set of states, $R ⊆ S × S$ represents the set of transitions and $s_1 ⊆ S$ represents the set of initial states.

事实证明，程序的模型检查通常是一个难题。 造成这种情况的部分原因是，许多模型检查算法都在努力寻求一种“完整性”形式，它们要么找到踪迹(trace)，要么返回证明这种踪迹不可能存在的证据。

  • trace: shows what statements are executed and in which order.

由于我们对生成测试用例感兴趣，因此我们更喜欢一种不同的方法：可能只有在很长时间执行后才能到达某个目标状态，或者根本无法到达，但是这些信息对我们构建测试用例没有帮助。 出于这个原因，我们引入了一个执行边界(execution bound) ，它描述了我们在分析程序时的深度。

使用这种执行边界的模型检查技术称为 有界模型检查(bounded model checking) ； 对于给定的边界 n，它们将返回一条跟踪信息或一条说明“无法在 n 步内达到目标状态”的语句。 因此，对于给定的边界，我们总是得到所有可以达到的状态的 近欠值(underapproximation， 即接近但没达到) ：我们当然可以在给定的范围内找到那些可以达到的状态，但是我们可以（may）(故意地？)错过只有通过更多步骤才能达到的状态。 相反，如果事实上有一种到达该状态的方法，我们将永远
不会声称某个状态在某个范围内是不可到达的

3.1.1. symbolic model checking 符号模型检测

  • The bounded model checking techniques used by the CPROVER framework are based on symbolic model checking, a family of model checking techniques that work on sets of program states and use advanced tools such as SAT solvers (more on that below) to calculate the set of reachable states.

3.1.2. How bounded model checking works

  1. Use bit vector representation to describe variables and operations on binary number
  2. transform to SSA
    1. we might modify the SSA form (i.e. introducing guard)
    2. thus finish encoding the behavior of programs as propositional formulas
  3. add ASSERT: describe the property we want to prove.
    1. To do this, we introduce a primitive ASSERT. Let e be some expression; then ASSERT(e) is supposed to do nothing if e evaluates to true, and to abort the program if e evaluates to false.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
// Origin
int max(int a, int b)
{
  int result;
  if (a < b)
    result = b;
  else
    result = a;
  return result;
}

// Bringing this into SSA form
int max(int a, int b)
{
  int result;
  if (a < b)
    result.1 = b;
  else
    result.2 = a;
  return Phi(result.1,result.2);
}

// As a first step, we modify the SSA form slightly by introducing an additional propositional variable C that tracks which branch of the if was taken. We call this variable the code guard variable, or guard for short
int max(int a, int b)
{
  int result;
  bit C; /* Track which branch was taken */
  C = a < b;
  /* if (C) - not needed anymore thanks to SSA */
    result.1 = b;
  /* else */
    result.2 = a;
  return Phi(C,result.1,result.2);
}
  • The resulting formula would be

    C = a<b and R1 = B and R2 = A and (C ⇒ return = R1) and ((not C) ⇒ return = R2).

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
// Origin
int max(int a, int b)
{
  int result;
  if (a < b)
    result = b;
  else
    result = a;
  ASSERT(result <= a); // Added
  return result;
}


// The corresponding SSA would be 
int max(int a, int b)
{
  int result;
  bit C; /* Track which branch was taken */
  C = a < b;
  result.1 = b;
  result.2 = a;
  ASSERT(Phi(C,result.1,result.2) <= a);
  return Phi(C,result.1,result.2);
}
  • We translate ASSERT(Phi(C,result.1,result.2) <= a) into

    Φ(C,result.1,result.2) <= a

  • The resulting formula would be

    C = a<b and R1 = B and R2 = A and (C ⇒ R1 <= A) and ((not C) ⇒ R2 <= A). (C ⇒ return = R1) and ((not C) ⇒ return = R2)

3.2. Incremental Bounded Model Checking

  1. BMC tools drop completeness (i.e., the ability to prove that a program does not contain a bug) in favor of falsification. They are used mainly to find bugs, as they can only prove the absence of bugs if the whole state space is explored (e.g., all loops have been fully unwound).
  2. In order to prove a program’s correctness, we need to compute the completeness threshold (CT), which can be smaller than or equal to the maximum number of loop iterations occurring in the program. However, computing CT to stop the BMC procedure and to conclude that no counterexample can be found is as hard as model checking the program
  3. When running a BMC tool, one usually has to specify a bound k explicitly; this will be used to limit the visited regions of data structures (e.g., arrays) or the number of loop iterations. This limits the state space to be explored during verification, but leaves enough for real errors in applications to be found.
  4. Since the best value for k is usually not known a priori先验, one must repeatedly run the BMC tool with increasing values of k; every increase of k will increase the number of loop iterations, the recursion depth, and the time and memory requirements. To check whether the value of k is big enough, BMC tools insert unwinding assertions after each loop. Failing these assertions does not mean that the program has a bug, but the verification is incomplete.

In ESBMC, there are two versions of incremental BMC

  1. CFG is unwound before the SSA generation by creating copies of the loop body and removing the backward GOTO instruction.
    1. The main difference between the static incremental BMC algorithm in ESBMC and the one described by Donaldson is the handling of nested loops.
    2. In both algorithms, the number of loop unwindings is set globally. However, nested inner loops are unwound first in ESBMC, while in Donaldson’s work outermost loops are unwound first.
  2. algorithm that incrementally unwinds the state transition system by running the symbolic engine with incremental numbers of unwinds.
    1. which allows incremental verification in many different configurations.
    2. Falsification/ Termination/ Incremental Verification/ k-Induction

3.2.1. Loop unrolling 循环展开

  • 循环展开（Loop unwinding或loop unrolling），是一种牺牲程序的大小来加快程序执行速度的优化方法。可以由程序员完成，也可由编译器自动优化完成。
  • 循环展开最常用来降低循环开销，为具有多个功能单元的处理器提供指令级并行。也有利于指令流水线的调度。
1
2
3
4
5
6
7
8
9
10
for (i = 1; i <= 60; i++) 
   a[i] = a[i] * b + c;

// 循环展开2次
for (i = 1; i <= 58; i+=3)
{
  a[i] = a[i] * b + c;
  a[i+1] = a[i+1] * b + c;
  a[i+2] = a[i+2] * b + c;
}

3.3. The k-induction Algorithm

…

4. 参考