[南京大学]-[软件分析]课程学习笔记(一)-introduction

南京大学 Static program analysis

introduction

1. program language and static analysis

编程语言：

• 理论
  • 语言设计
  • 类型系统
  • 语义和逻辑
  • …
• 环境
  • 编译器
  • 运行时系统
  • …
• 应用
  • 程序分析
  • 程序验证
  • 程序合成
  • …

背景：在过去的十年中，语言的核心基本没有变化，但是程序变得显著的更大和更复杂；

挑战：如何确保大规模复杂程序的可靠性、安全性和其他承诺

2. why we learn static analysis

程序的可靠性reliability：

• null pointer dereference 空指针引用
  • 去引用的时候没有define，就会带来很多bug
• memory leak 内存泄漏
  • malloc没有free，内存占用过多会导致crash

程序的安全性security：

• private information leak 私有信息的泄露
• injection attack 注入攻击

编译器优化

• dead code elimination 死代码消除
• code motion 代码移动

程序理解

• IDE call hierarchy 调用层次
• type indication 类型指示

3. what is static analysis

Static analysis analyzes a program P to reason about its behaviors and determines whether it satisfies some properties before running P.

静态分析通过分析程序P来推理其行为，并在运行P之前确定其是否满足某些属性

• Does P contain any private information leaks?
• Does P dereference any null potinters?
• Are all the cast operations in P safe? 类型转换操作符
• Can v1 and v2 in P point to the same memory location?
• Will certain assert statements in P fail?
• Is this piece of code in P dead(so that it could be eliminated)?

Rice theory 莱斯定理: 不存在一个方法可以确定的给出一个程序是否满足一些非平凡属性的判断。

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

r.e. (recursively enumerable) = recognizable by a Turing-machine
递归可枚举的语言就是图灵机可识别的语言

non-trivial 不简单，重要

以上表述为一个perfect static analysis是不存在的

从学术的角度来看，一个perfect的static analysis需要满足以下两个条件：

• sound：over approximate 包含true
• complete: under approximate true包含

所以并不追求完美的静态分析，而是追求useful static analysis：

• Compromise soundness（false negatives）折中的漏报控制
• Compromise completeness (false positives) 折中的误报控制

Mostly compromising completeness: Sound but not fully-precise static analysis

绝大多数静态分析追求的都是追求Soundness，会造成误报

Soundness is critical to a collection of important(static-analysis) applications such as compiler optimization and program verification.

Static analysis: ensure (or get close to) soundness, while making good trade-offs between analysis precision and analysis speed.

确保soundness，并在分析精度和分析速度之间做好权衡

4. static analysis features and examples

Abstraction + Over-approximation

抽象和过近似

• abstraction
• over-approximation
  • transfer function
  • control flows

Example:

判断给定的程序中所有变量的符号：正、负或者是0.

• T：unknow 可正可负（over-approximation 过近似）
• bottom：undefined，除零操作，抛出异常操作

transfer function定义了如何在抽象值上评估不同的程序状态，并且应该根据分析问题和不同程序状态的语义去定义

• 1问题是除零、抛出异常，则应该为undefined；
• 2问题是下标为负，抛出异常，也应该为undefined
• 3问题则是over-approximated，也即是误报，在实际的程序中a=x+y=9,所以并不会报错，而在抽象化为符号的过程中会模糊这个界限，导致产生误报

控制流分析，y的两个值是两个branch，执行分支不同会使z的值产生变化。并且在实际中枚举所有路径是不可能的，空间特别庞大，因此flow merging则被很多静态分析采用。