0%

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

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

PL知识体系

image-20200802113608162

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

Rice’s Theorem(莱斯定理)

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

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

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

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

由莱斯定理,分析时出现sound和complete情况,存在两种妥协方案:

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

误报(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. 每一语句最多有三个“地址”(变量,常量)

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节点