软件分析

导论

2020-02-26 10:22 CST
2020-02-26 10:22 CST
CC BY-NC 4.0
  • 程序语言
    • 理论
      • 语言设计
      • 类型系统
    • 环境
      • 编译器
      • Runtime system
    • 应用
      • 程序分析
      • 程序验证

背景:过去几十年,语言的内核只有很少的变化,但是语用环境变化,程序变得越来越大并且更加复杂

挑战:如何保证可靠性、安全性和其他期望在更大范围和更复杂的程序中

  • 为什么需要静态分析:
    • 程序可靠性:空指针,内存泄漏等
    • 程序安全性:私有信息泄露,injection attack,etc
    • 编译优化:Dead code elimination,code motion,etc
    • Program Understanding: IDE call hierarchy,type indication,etc

Static Analysis

Static analysis analyzes a program P to reason about its behaviors and determines whether it satisfies some properties before running P . 但是根据Rice ‘s Theorem,并没有一个方法能够准确的判断有或没有。动态运行时行为有关的行为无法准确判断,即perfect static analysis 不存在。

  • perfect static analysis:同时满足sound 和 complete

    • sound: over approximate,报出来的一定包括所有truth但是可能有假的
    • complete: under approximate,报出来的一定没有假的但不完全包括truth
  • Useful Static Analysis

    • compromise soundness(false negatives):妥协soundness保证completeness,会带来漏报
    • compromise completeness(false positives):妥协completeness,会带来误报
    • 在绝大多数分析中,几乎所有都是妥协completeness保证sound

Static Analysis: Bird’s Eye View

	if(input)
		x=1;
	else
		x=0
-> x = ?

上有两种分析结果:

  • when input is true, x=1 when input is false, x=0
  • x = 0 or x = 1

这两种结论都是正确的,前者是sound,precise,expensive,后者是sound,imprecise,cheap,甚至可以说x=0 or 1 or 2 or 3这种结果也是正确的,因为保证了sound

Static Analysis:在保证soundness的情况下,在precisionanalysis speed之间做出一个平衡

Over-approximation

Transfer Functions

  • transfer functions 在抽象指令上进行定义

  • 根据程序的语义来设计

unknown: $\top$

undefined: $\bot$

Control Flows