2021.11.11 组会（程序分析的基本原理）

"主讲人：玄跻峰老师"

概述

input -> output

program analysis 包含 front-end 和 back-end，front-end 包括 lexical analysis 和 syntax analysis；

program analysis 包含 static / dynamic analysis；

int func(int x) {
    if (x > 0) {
        printf("1-1");
        x++;

        if (x < 0) {
            x--;
        }
    }
    printf("1-2");
}

在上面的代码段中，可以抽象出的 model 是：t1(x > 0) ^ t2(x ++) ^ t3(x < 0) -> model checking

应用

e.g. instrumentation (插桩)：如输出运行到的代码行的行号

debugging

比如 gdb 等 debug 工具，其中的实现包含了程序分析。

test (test case generation)

• coverage
  • focus on the divesity of test cases
• fault detection
  • focus on a particular path
• reproduction
  • find a particular path
• program sythesis
  • program -> program
  • includes program repair and program complete
• program transformation

工具

分析程序结构的工具，输出 AST。

C / C++	Java	C#
LLVM + Clang	- Eclipse JDT - SOOT (将 java 编译为 jimple) - Spoon (直接在源代码上操作) - WALA (稳定但是功能弱；用于切片)	Roslyn

难点 & 方案

1. 当代码中涉及到 networking resources, drivers, database/file，以及代码中有时序逻辑时，很难进行准确建模
   1. removal (忽略) -> model 不匹配
   2. hard-coding (硬编码) -> how to?
2. if (x = g(y) > 0) 其中 g(y) 为库函数，导致无法准确建模

model 不准确 -> 建立一个 model，映射到正确的 model 上

术语

我们使用程序分析工具找到了 5 个地方可能存在 bug，最终发现 5 个中有 2 个确实为 bug，3 个不为 bug，同时还有 1 个 bug 没有找到。

• soundness (可靠性)：2 / 5
• true positive: 2 (找到的 2 处 bug)
• false positive: 3 (找错的 3 处)
• false negative: 1 (未找到的 1 处 bug)
• recall -> completeness (完备性)：2 / 3 (找到的bug数 / 总bug数)

有无检测到	相关的（bug）	不相关的（非 bug）
被检索到的	true positive	false positive
未被检索到的	false negative	true negative