0%

静态程序分析课程笔记(简介)

母校计算机院的李樾、谭添老师讲的课,听了第一节课就哭了,决定做一下笔记,课程网站 https://pascal-group.bitbucket.io/teaching.html。

PL知识体系

image-20200802113608162

如上图所示,主要分三大块,理论部分包含语言设计、类型系统、语义和逻辑检查;环境部分包含编译器和运行时设计等;应用部分包含程序分析、程序验证和程序生成等,本课程主要关注于应用方面的程序分析。

Rice’s Theorem(莱斯定理)

停机问题

了解莱斯定理,首先证明停机问题是不可判定的:

  • 假设存在停机问题的判定算法 bool Halt(p)

  • 存在恶意程序:

    1
    2
    3
    4
    5
    6
    void Evil() {
    if (Halt(Evil))
    while(1);
    else
    return;
    }
  • 那么Halt(Evil)返回存在矛盾:

    • 若返回真,即evil可停机,那么Evil()走if分支,但该分支evil不可停机,矛盾;
    • 若返回假,即evil不可停机,那么Evil()走else分支,但这样evil可以停机,矛盾。

内存泄露问题

内存泄露问题与之类似:

1
2
3
4
5
6
7
void Evil() {
int a = malloc();
if (LeakFree(Evil))
return;
else
free(a);
}

Rice定理

经过上面两个问题,可以感觉到只要是一个判定问题,就可以套用上面的evil框架来反证这个框架是不可判定的,Rice定理对上面情况作了总结:

Any non-trivial property of the behavior of programs in a i.e. language is undecidable.

对递归可枚举语言来说,不存在一个完美(Sound&Complete)的,用于判定程序中non-trivial的属性的方法。

这里“non-trivial property”可以理解为程序分析的种种目的,如变量是否空指针、是否存在信息泄露等。

  • 平凡(trivial)属性:对图灵机(语言)P来说,要么对全体程序都为真,要么对全体程序都为假;
  • 非平凡(non-trivial)属性:不是平凡的所有属性,如停机问题、空指针、信息泄露等。

证明:

设给定函数上有非平凡性质P,假设空集(对任何输入都不输出的程序,包括不停机程序)不满足P,因为P非平凡,因此一定有满足P的程序ok_prog;

假设有判定性质P的算法 P_holds(),编写以下程序判断程序q是否停机:

1
2
3
4
5
6
7
Bool halt(Program q, Input w) {
void evil(Input x) {
q(w);//如果q不停机,那么evil不满足P
ok_prog(x); //如果q停机,那么启动ok_prog,此时evil程序等同于okprog程序
}
return P_holds(evil);
}

上面程序借用了P_holds的能力来判断停机问题,关键在于evil:

  • 如果q(w)不停机,那么因为不停机程序不满足P,evil()不满足P;

  • 如果q(w)停机,那么evil(x)等同于ok_prog(x)evil(x)满足P

综上,只要判定evil(x)是否满足P,就可判定停机问题,但是之前已经证明过,停机问题是不可判定问题,因此矛盾。

注意,将空集描述为满足P,也可以用类似的方法证明(设有不满足P的程序no_prog…)

可靠性和完备性(soundness&completeness)

莱斯定理说明了不可判定性,在实际分析时只能做may或者must的分析,分析时出现sound和complete情况,存在两种妥协方案:

  • Compromise soundness:妥协可靠性,即接受误报(may),该方案是静态分析较常见
  • Compromise completeness:妥协完备性,即接受漏报(must)

误报(False positive)与漏报(False negative)关系如下图所示:

image-20200802115612020

简单的程序分析案例

分析在代码p处变量v的正负(+, -, 0)。

定义数据抽象

  • $+$:正
  • $-$:负
  • $0$:零
  • $\top$:未知
  • $\perp$:未定义

定义Transfer Function

即读取一个二元操作statements,输出符号是什么,如下表:

image-20200802154058197

定义Control Flow Merge

在CFG中汇聚点中要合并情况
image-20200802154239519

编译器vs.静态分析器

  • 编译器:
    词法分析(产生tokens)→语法分析(产生AST)→语义分析(包括类型检查,产生Decorated AST)→翻译(产生IR)→代码生成

  • 静态分析:
    静态分析基于IR

AST和IR

AST

  1. 符合语法结构
  2. 依赖于特定语言
  3. 适合于类型检查
  4. 缺失控制流信息

IR

  1. 接近机器代码
  2. 语言无关
  3. 含有控制流信息

三地址码

一种常用的IR:

  1. 右侧只有一个操作
  2. 每一语句最多有三个“地址”(地址可以是变量,常量)
    • $z=x\text{ }op\text{ }y$
    • $x=op\text{ }y$
    • $x=y$
    • $goto\text{ }L$
    • $if\text{ }x\text{ }goto\text{ }L$
    • $if\text{ }x\text{ }op\text{ }y\text{ }goto\text{ }L$

Soot 中的三地址码:

  • @parameter:函数参数
  • $x:临时变量

  • <method signature>:类+返回值类型+方法名+函数参数类型

  • <init>:构造函数
  • <clinit>:类初始化函数(静态变量初始化等)
  • invokespecial:调用构造函数、父类方法、私有方法
  • invokevirtual:实例方法调用(virtual dispatch)
  • invokeinterface:不能优化、调用接口、检查接口实现
  • invokestatic:调用静态方法
  • invokedynamic:运行其他动态语言

SSA

一种特殊的三地址码:

  • 每次赋值有新的变量名
  • 每一个变量都有唯一定义

优势:

  • flow-insensitive analysis更准确
  • 容易做优化算法

劣势:

  • 引入大量变量
  • 编译时有性能问题

Control Flow Graph

Basic Block是CFG的主体。

  • Basic Block:一个最长的语句序列,并保证入口只能在最开始指令且出口只能在最后一个指令

构造Basic Blocks

  • Input:程序P的三地址码序列
  • Output:程序P的basic blocks

  • 算法

    1. 确定leaders(每个basic block的头)

      • 序列中的第一个指令
      • 跳转指令的目标指令
      • 跳转指令的下一条指令
      • return指令
    2. 每个Basic Block包含其leader至下一个leader前的所有语句

构造CFG

  • 添加边,在以下两种情况下:
    • 代码块存在先后顺序,且不存在无条件跳转
    • 每个跳转间
  • 添加entry和exit节点