DySy

这篇paper的完整题目是 DySy: Dynamic Symbolic Execution for Invariant Inference

下载链接

Motivation

• 精简化 Daikon 所识别的 invariants
  • 一旦用户开始拓展给定的 invariant 的范围，各种 possible invariant 的总量就会急剧增长，超出正常人的理解能力
  • 以至于用户每次只能推断极少的几个简单的 invariant
• 另外，需要相当完整的输入值才能正确推断 invariant
• 其他的 paper 需要预先给定 invariant 的模式

Intro

• 本文的方法将会
  • 大幅提高“推断的 invariant”的有效性
  • 减少测试用例的规模
• Daicon 非常火
  • 我们无法“证明”某个 invariant 正确，只能通过“高置信度”来推断
  • invariant 可能不仅来源于程序本身，还有输入值的特定结构
    • 因此 Daicon 这种方法更有效了（？）
• 使用 concolic 进行程序执行，获得 PC

int testme(int x, int y) {
	int prod = x*y;
	if (prod < 0)
		throw new ArgumentException();
	if (x < y) {
		// swap
		int tmp = x;
		x = y;
		y = tmp;
	}
	int sqry = y*y;
	return prod*prod - sqry*sqry;
}

• 本文可以推断出的结果
  • precondition x*y > = 0
  • postcondition \result == (((x < y) -> y*x*y*x - x*x*x*x) else -> (x*y*x*y - y*y*y*y))
• 相比之下，Daicon 只能生成var >= 0或者var == 0这种结论
  • 除非 Daicon 有一个非常全面的测试用例

2、文章定位

• 本文的 symbolic execution 并不是 DART 和 CUTE 文中的 concolic execution，因为本文的 symbolic execution 不会为变量生成新的值

3、背景

3.1 Dynamic Invariant Inference: Daikon

• Daicon 是目前最成熟、最广泛应用的工具
• 生成大量的 invariant 信息，并且排列组合生成更多

3.2 符号执行

• 文章把 PC 定义为

the accumulator of properties which the inputs must satisfy in order for an execution to follow the particular associated path

• 因此，本文把 PC 当做一个 path 的 precondition
• 符号执行的一个难点是，给 PC 添加一个新的 predicate后，这个 PC 是否还有解
  • 一般使用 automatic theorem prover 进行解答

4、方法

• 符号变量包括
  • class instance
  • static variables
  • the method’s parameters
  • the method’s result
• PC 只由 concrete execution 决定
  • 每个具体的 test case 都有 PC，那么这个 PC 就是这个 test case 的 pre/postcondition
  • 运行所有 test case 的运行结果，用 symbolic reasoning 获得简化的 invariants

StackAr例程

public Object top() {
	if(Empty)
		return null;
	return theArray[topOfStack];
}

• 输出 precondition
  • Empty = true || (Empty = false && topOfStack >= 0 && topOfStack < theArray.Length)
• 输出 postcondition
  • Empty = true ==> (\result = null)
  • (Empty = false && topOfStack >= 0 && topOfStack < theArray.Length) ==> (\result = theArray[topOfStack])

• 每个 invariant 推断工具都应该具有抽象化的能力
  • 比如，Daikon 和 DIDUCE 一般把各个具体输入值i = 1 || i = 2 || ... || i = 1000推广为i > 0
  • 但是 DySy 的方法是直接使用 PC，也就是已经推广化的 invariants，因此更加精确
• DySy 可以获取“深层”的 invariants，比如pure这个 postcondition （意思是 no side-effect）
  • 相比之下，Daikon 把程序当做黑盒，提取的信息更 shallow

void allInts(int i) {
	if (i < 0)
	{ ... } // do something
	else if (i == 0) { ... } // do something else
	i++;
	if (i > 1) { ... } // do something else
}

• 这个例子展示了 symbolic reasoning engine（theorem prover）的重要性
  • 正常的 precondition 应该是 true
  • 2B的 precondition 是 ((i < 0) && !(i+1 > 1)) || (!(i < 0) && (i = 0) && !(i+1 > 1)) || (!(i < 0) && !(i = 0) && (i+1 > 1))

4.2 具体实现

• 使用 Pex framework
  • 功能类似 DART
  • 在一个 feedback loop 里面，不断的尝试访问新的路径

5、测评

• 本文使用 Daicon 界流行的StackAr程序作为 benchmark

• Previous
  JPF安装
• Next
  iDiscovery