【软件分析/静态分析】学习笔记01—

这篇具有很好参考价值的文章主要介绍了【软件分析/静态分析】学习笔记01——Introduction。希望对大家有所帮助。如果存在错误或未考虑完全的地方，请大家不吝赐教，您也可以点击"举报违法"按钮提交疑问。

🔗 课程链接：李樾老师和谭天老师的：南京大学《软件分析》课程01（Introduction）_哔哩哔哩_bilibili

一、静态程序分析介绍

1.1 PL and Static Analysis 程序语言和静态分析

1.2 为什么要学 Static Analysis?

1.3 什么是静态分析 ?

1.4 静态分析的特征和例子

1.4.1 sound and complete （no perfect static analysis）

1.4.2 false negatives or false positives (useful static analysis)

1.4.3 Static Analysis 例子 — Bird's Eye View

1.5 静态分析大致步骤—举个例子🌰

1.5.1 Abstraction（抽象）

1.5.2 Over-approximation(近似): Transfer Functions（转换函数）

1.5.3 Over-approximation(近似): Control Flow（控制流）

1.5.4 总结

一、静态程序分析介绍

1.1 PL and Static Analysis 程序语言和静态分析

PL (Programming Languages, 程序语言)

Static Analysis（静态分析）

如下图所示，PL可以分为三个主题：理论、环境和应用

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

【软件分析/静态分析】学习笔记01——Introduction

程序语言的分类：

命令形语言：C、Java
函数式语言：JavaScript、
逻辑式语言：一条条逻辑声明出来的语言

挑战：
这么多年来，语言的核心没有变，但是软件越来越复杂，如何保证大规模复杂程序的安全性、可靠性……？

1.2 为什么要学 Static Analysis?

从代码层面来看，静态分析可以做很多事情，后续也会详细讲到：

对程序可靠性Program Reliability
空指针引用 null pointer dereference，内存泄漏 memory leak……
对安全性 Program Security
私有信息泄露 private infomation leak, 注入攻击injection attack……
编译优化 Compiler Optimization
死代码消除 Dead code elimination，code motion……
程序理解 Program Understanding
IDE call hierarchy, type indication……

对于程序员，静态分析可以帮助写更高质量的代码。

1.3 什么是静态分析 ?

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

静态分析(static analysis) 是在程序运行之前，分析其行为，确定它是是否能满足某些特性要求：

有没有一些程序泄露
有没有空指针引用异常?
所有的变量variable 用之前都初始化了吗？
所有的cast operation是安全的吗？
v1和v2会不会指向相同的内存地址？
程序中的断言语句 assert 会失败吗？
死代码？
……

但是，根据Rice' Theorem（大米定理/莱斯定理），不存在一个方法可以给出一个确切的答案Yes or No，原文如下：

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

这句话里的一些词：

r.e.(recursively enumerable) = recognizable by a Turing-machine
r.e. language: 递归可枚举的语言（图灵机可识别的语言，可以理解为现代的编程语言，C 、JAVA）
non-trivial property：≈ 一些有趣/有价值的性质 ≈ 与动态运行时行为runtime behaviors相关的性质，就像前边列举的空指针、内存变量什么的。
undecidable: 给不出确切答案

可以这么理解：

一个递归可枚举的语言（图灵机可识别的语言，可以理解为现代的编程语言，C 、JAVA），他的一些non-trivail property（与程序运行时行为相关的性质，例如是否有空指针、有没有内存泄漏）是不能确定的（例如不能准确地说有空指针或者没有）。

再学术一点的理解：

一个完美的静态分析(perfect static analysis) 是满足 sound and complete 的（sound 和 comlete是静态分析的两个特征，见1.4.1）.
大米定理就是在告诉我们，不存在完美的静态分析，可以准确地回答Truth，也就是不能同时满足sound 和 complete.

1.4 静态分析的特征和例子

为什么没有一个perfect的呢，因为一些情况其实不可避免，导致分析要么太“过”(sound)，要么太“保守”(complete)。

1.4.1 sound and complete （no perfect static analysis）

【软件分析/静态分析】学习笔记01——Introduction

如图所示，complete和sound的关系：

truth：是这个程序中理论上的所有的正确的答案
complete：指的是，报出来的，都是对的，但是不全
sound：包含了所有正确答案，

1.4.2 false negatives or false positives (useful static analysis)

既然没有perfect静态分析，为什么还要去研究呢？因为可以对一方妥协，由此就有了useful static analysis（有用的静态分析）。

Useful static analysis：

Compromise soundness (false negatives，假阴性) : 妥协soundness，就是不sound，会产生漏报（错的没检测到）
Compromise completeness(false positives，假阳性)：妥协completeness，不complete，会产生误报（对的说是错的）

在绝大Useful静态分析中，我们所研究的更多是妥协completeness：要求分析是 Sound 的，虽然并不全都准确（not fully-precise）（宁可错杀100不可放过一个），可以误报，但是不能漏。

soundness越好，分析就越好。

1.4.3 Static Analysis 例子 — Bird's Eye View

如下图，对左侧的代码进行分析的时候，产生的2个分析结果

【软件分析/静态分析】学习笔记01——Introduction

这两个分析结果都是对的，没有产生漏报，都满足sound，且：
                1 更准确但是昂贵；
                2 不够准确但是cheep;
还有一些可能的分析结果如下:
                3. x = 0, 1, 2, 3, 4
                4. x = 1, 2, 3, 4
        其中，3产生了误报，都是涵盖了所有情况，也是sound，是对的；都是4漏了0，是错误的。

一句话概括静态分析：

静态分析是在确保（or 尽量接近）soundness的同时，在分析精度(precision)和速度(speed)之间做一个平衡，这才是一个Useful 静态分析