forked from RangerNJU/Static-Program-Analysis-Book
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
GitBook: [master] 26 pages and 2 assets modified
- Loading branch information
1 parent
043cc96
commit 9eb2d16
Showing
30 changed files
with
612 additions
and
285 deletions.
There are no files selected for viewing
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
File renamed without changes
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,12 +1,131 @@ | ||
# Static-Program-Analysis-Book | ||
# 简介 | ||
|
||
[Gitbook在线阅读地址](https://ranger-nju.gitbook.io/static-program-analysis-book/) | ||
[《静态程序分析》Gitbook在线阅读地址](https://ranger-nju.gitbook.io/static-program-analysis-book/) | ||
|
||
[GitHub项目地址](https://github.com/RangerNJU/Static-Program-Analysis-Book) | ||
|
||
---- | ||
[《静态程序分析》GitHub项目地址](https://github.com/RangerNJU/Static-Program-Analysis-Book) | ||
|
||
Getting started with static program analysis. Read this and start writing your first static program analyzer! | ||
|
||
静态程序分析入门。阅读此书并着手编写你的第一个静态程序分析器吧! | ||
|
||
# 这一《静态程序分析》教程对谁有用? | ||
|
||
学生,开发者,研究者……几乎所有当代生活者都能从中受益。 | ||
|
||
- 学习方向与程序有关的**学生。** | ||
- 计算机方向的学生可以通过深入学习这一领域知识而为自己建立独特的学术和就业优势。 | ||
- 其他方向的学生同样可以通过了解这一技术,了解静态分析软件能够为你提供怎样的功能和便利,以及如何更好地使用这些软件以保证你所关心的程序质量。 | ||
- 工作内容与程序有关的**开发者。** | ||
- 无论你希望更好地理解[Wiki](https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis)上众多的开源或是闭源的静态程序分析技术,还是希望自己开发一个适用于眼下工作内容的静态程序分析器以保证程序质量,了解静态程序分析都会有所帮助。 | ||
- 研究领域与程序相关的**研究者。** 或许你希望微调研究方向,却因没有合适的入门材料而苦恼;或许你希望了解计算机领域的相关知识以期获得启发……这一教程可以作为你的入门材料或是闲暇读物。 | ||
- 生活与程序相关的**每个人** | ||
- 软件质量是信息化时代的重要议题之一,在这个时代生活与工作,你一定会遇到相关的问题。 | ||
- 在大多数学校和企业中,没有开设该领域的课程。 | ||
|
||
# 什么是静态程序分析? | ||
|
||
## 静态程序分析在计算机科学领域中的定位 | ||
|
||
<img src=".gitbook/assets/PL.png" style="zoom: 50%;" /> | ||
|
||
**静态程序分析**是**编程语言**中**应用**层面下的一个细分领域。它是一个非常重要的核心内容。 | ||
|
||
在理论部分,研究者考虑的是如何设计一个语言的语法和语义,如何设计语言的类型系统等等问题;有了语言的语法、语义和类型系统之后,我们需要支撑语言的运行。因此,在环境部分,研究者考虑的是如何为运行中的程序提供运行时环境——如何设计编译器,在运行时需要怎样的支持(如内存的分配管理)等等;应用部分则关注如何保证语言所写出程序的效率、安全性和可靠性,研究者们考虑如何对程序进行分析,验证和合成(如何自动合成一个程序)。 | ||
|
||
### 编程语言的分类 | ||
|
||
当今的计算机世界,面对这样一条恶龙: | ||
|
||
> 数十年来语言的核心没有变化,但软件的规模和复杂性增长迅速,如何保证程序的可靠性? | ||
尽管新的语言和特性层出不穷,但现在编程语言无非三大类 *(如果你对其中的某个语言不熟悉,可以到语言的官网或英文Wiki页面查看相关示例,也可以利用搜索引擎做初步的了解。<u>本教程内容主要关注于针对命令式语言JAVA的分析。</u>)* : | ||
|
||
* 命令式(C、C++、JAVA) | ||
* 函数式([Scala](https://www.scala-lang.org/)、[Haskell](https://www.haskell.org/)) | ||
* 逻辑式([Prolog](https://en.wikipedia.org/wiki/Prolog)) | ||
|
||
## 静态程序分析的应用 | ||
|
||
|
||
静态程序分析即是屠龙的宝刀之一,这一技术可以处理以下问题(*以下概念只需要了解,重要的应用在后文中会详细讲解。*): | ||
|
||
1. 提高程序可靠性 | ||
- Null pointer dereference, memory leak, etc. | ||
- 空指针引用与内存泄漏等:几乎每个程序编写者都被这两个问题所困扰过 | ||
2. 提高程序安全性 | ||
- Private information leak, injection attack, etc. | ||
- 隐私信息泄漏:TODO | ||
- [注入攻击](https://en.wikipedia.org/wiki/Code_injection):这是网络安全中非常常见的议题。不熟悉的读者可以查看[W3School](https://www.w3schools.com/sql/sql_injection.asp)或[Wiki](https://en.wikipedia.org/wiki/SQL_injection)上关于SQL注入攻击的例子。 | ||
3. 为编译优化提供基础技术 | ||
- Dead code elimination, code motion, etc. | ||
- [死代码消除](https://en.wikipedia.org/wiki/Dead_code_elimination):在编译器的机器无关优化环节,将不会对程序执行结果产生影响的代码(即死代码)删除。 | ||
- [循环不变量的代码移动](https://en.wikipedia.org/wiki/Loop-invariant_code_motion):在编译器的机器无关优化环节,在保证不影响程序执行结果的情况下,将循环中的特定语句移动到循环外,使得程序运行时执行的语句数减少。更为详细的解释可以参考[StackOverFlow上的回答](https://stackoverflow.com/questions/5607762/what-does-code-motion-mean-for-loop-invariant-code-motion)。 | ||
4. 有助于程序理解 | ||
- IDE call hierarchy, type indication, etc. | ||
- 为集成开发环境的功能提供帮助:当你使用VS 2019/Idea/Clion/Eclipse/Android Studio等等IDE时,将鼠标悬停在代码上,IDE能够动态地分析并提示你所悬停对象的相关信息,背后使用的技术就是静态程序分析。 | ||
|
||
## 静态程序分析的市场 | ||
|
||
<img src=".gitbook/assets/market.png" style="zoom: 33%;" /> | ||
|
||
- 在学术界,静态程序分析技术<u>几乎可以应用于所有关于程序的研究方向。</u> | ||
- 在工业界,国外的Google,IBM等大企业已经初步建立了自己的静态程序分析团队。国内的华为和阿里等企业也正在积极寻找静态程序分析方面的人才。 | ||
- **无论你将来想在学术界还是工业界深入发展,学习这一领域的知识都能为你建立独特的优势。** | ||
|
||
## 静态程序分析与类似技术的对比 | ||
|
||
> Testing shows the presence, not the absence of bugs. --Edsger W. Dijkstra | ||
动态的软件测试和形式化语义的验证的作用与静态程序分析类似,这一部分对这三个细分方向做简单的对比。 | ||
|
||
### 静态程序分析 | ||
|
||
- 优点:在选定的精度下能够保证没有bug。这在教程中会详细介绍。 | ||
- 缺点: | ||
1. 学术门槛相对高。目前国内高校只有北京大学和南京大学开设有关课程,且暂无教材。作为一门计算机专业的高年级选修课,入门和提高都较困难。 | ||
2. You tell me. | ||
|
||
### 动态软件测试 | ||
|
||
- 优点:在工程中被广泛应用,并且有效。实现简单,便于自动化。 | ||
|
||
- 缺点: | ||
|
||
1. **无法保证没有bug。** 这是无法遍历所有可能的程序输入的必然结果。 | ||
2. 在当今的由多核与网络应用带来的**并发环境下作用有限。** 某个bug可能只在特定情况下发生,因而难以稳定地复现。如果你对并发程序的测试细节感兴趣,可以参考[《拧龙头法测试并发程序》](https://zhuanlan.zhihu.com/p/51341151)。(截图来自南京大学《形式化语义》课程资料) | ||
|
||
<img src=".gitbook/assets/concurrentProgram.png" style="zoom: 67%;" /> | ||
|
||
### 形式化语义验证 | ||
|
||
- 优点:由于用数学的方法对程序做了抽象,能够保证没有bug。 | ||
|
||
- 缺点: | ||
|
||
1. 学术门槛较高,学习者必须有良好的数学基础才能入门。 | ||
|
||
2. 验证代价较高,一般来说非常重要的项目会使用这一方式保证程序质量。甚至在操作系统这样重要的软件中,也并不一定会使用。(截图来自鸿蒙OS直播发布会) | ||
|
||
<img src=".gitbook/assets/harmonyOS.png" style="zoom: 67%;" /> | ||
|
||
# 加入项目/How to contribute | ||
|
||
> 觉得有所帮助的话可以点个star支持哦。 | ||
欢迎希望添加更好的讲解资料或对教程内容进行扩充的小伙伴 `fork, modify, PR` 三连。 | ||
|
||
# 本地化/Localization | ||
|
||
## English | ||
|
||
If you wanna translate this project into English, I can proofread for you. All you need to do is `fork, modify, PR` . | ||
|
||
## 日本語 | ||
|
||
このプロジェクトを日本語に翻訳したい場合は、翻訳されたコンテンツの校正をお手伝いします. `fork, modify, PR` で始めましょう! | ||
|
||
# 其他相关项目 | ||
|
||
[《软件测试简介》Gitbook在线阅读地址](https://ranger-nju.gitbook.io/software-testing-intro) | ||
|
||
[《软件测试简介》GitHub项目地址](https://github.com/RangerNJU/Software-Testing-Intro) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,15 +1,20 @@ | ||
# Table of contents | ||
|
||
* [第零章-写在前面](src/ch0/README.md) | ||
* [静态程序分析是啥玩应啊](src/ch0/00-01-why-SPA.md) | ||
* [为什么是这本书?](src/ch0/00-02-why-this-book.md) | ||
* [来源与版权信息](src/ch0/00-03-sources-and-license.md) | ||
* [第一章-静态程序分析简介](src/ch1/README.md) | ||
* [初见——静态分析是什么?](src/ch1/01-01-whats-spa.md) | ||
* [中间表示——静态分析器的输入](src/ch1/01-02-ir.md) | ||
* [第二章-数据流分析的理论与应用](src/ch2/README.md) | ||
* [数据流分析](src/ch2/02-00-dataflow-analysis.md) | ||
* [到达定值分析](src/ch2/02-01-reaching-def-analysis.md) | ||
* [活跃变量分析](src/ch2/02-02-live-var-analysis.md) | ||
* [可用表达式分析](src/ch2/02-03-available-exp-analysis.md) | ||
* [简介](README.md) | ||
* [第零章-写在前面](ch0/README.md) | ||
* [为什么是这本书?](ch0/00-01-why-this-book.md) | ||
* [来源与版权信息](ch0/00-02-sources-and-license.md) | ||
* [第一章-静态程序分析简介](ch1/README.md) | ||
* [初见——静态分析是什么?](ch1/01-01-whats-spa.md) | ||
* [中间表示——静态分析器的输入](ch1/01-02-ir.md) | ||
* [第二章-数据流分析——应用](ch2/README.md) | ||
* [数据流分析](ch2/02-00-dataflow-analysis.md) | ||
* [到达定值分析](ch2/02-01-reaching-def-analysis.md) | ||
* [活跃变量分析](ch2/02-02-live-var-analysis.md) | ||
* [可用表达式分析](ch2/02-03-available-exp-analysis.md) | ||
* [第三章-数据流分析——理论](ch3/README.md) | ||
* [数据流分析](ch3/03-00-dataflow-analysis.md) | ||
* [到达定值分析](ch3/03-01-reaching-def-analysis.md) | ||
* [活跃变量分析](ch3/03-02-live-var-analysis.md) | ||
* [可用表达式分析](ch3/03-03-available-exp-analysis.md) | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
# 为什么是这本书? | ||
|
||
> 这里的《静态程序分析》跟别处的有什么不同? | ||
## 为什么应该读这本书? | ||
|
||
**1. 当前,中英文社区都缺乏这一领域的入门材料。** | ||
|
||
**2. 本书将试图通过理论和实践的结合介绍这一领域。** | ||
|
||
### 中文社区 | ||
|
||
在搜索引擎上搜索相关中文关键词,你会发现结果靠前的答案都是与某南的李老师相关的课程在B站上公开视频的笔记,其中有不少写得很好,**但并非面向一般学习者开发者的教程**。这两者有重要的区别: | ||
|
||
* 笔记:**面向自己复习**使用,只要自己回顾时能迅速pick up当时理解到的重点,就是一份好的笔记。 | ||
* 教程:**面向他人学习**使用,一份好教程能让学习者迅速把握领域中的重点,并且为学习者的进一步应用打下基础。 | ||
|
||
### 英文社区 | ||
|
||
在搜索引擎上搜索英文关键词,你应该能搜索到国际上的大牛们的教材式的PDF文件和相关论文,或是开源的静态分析程序。但同样**缺乏教程**。大多数材料要么艰涩难懂要么太过粗浅。根据粗略的访问与调查,目前业界中主要还是大型的、国际化的、有前瞻视野的企业重视这一技术的发展应用,而中小企业则对其并不了解或认为静态程序分析技术仍不成熟。 | ||
|
||
### 理论与实践的结合 | ||
|
||
本书将同时涉及理论和实践,这主要是受到了《The Rust Programming Language》的启发。 | ||
|
||
### 本书写作的目标 | ||
|
||
能让大多数有一定编程经历,已经修过本科计算机相关基础课程的大四及以上同学: | ||
|
||
1. 在阅读本书时能较为轻松地理解理论 | ||
2. 能够自主完成一个简单的程序实现 | ||
3. (任何人都)能在阅读过程中接触计算机不同领域的小知识 | ||
|
||
## 为什么要写这本书? | ||
|
||
* 最主要的动力还是老师现场授课时我感受到的passion | ||
* 这是一个少有人涉足的领域,写这方面的内容很符合我的性格 | ||
* 我从开源社区中获益颇多,找到了合适的机会也希望能为开源社区(尤其是中文社区)作出自己的贡献 | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
# 来源与版权信息 | ||
|
||
## 资料来源 | ||
|
||
本入门教程主要内容基于南京大学《软件分析》课程。 | ||
|
||
[PASCAL研究组主页](https://pascal-group.bitbucket.io/teaching.html) | ||
|
||
## 版权信息 | ||
|
||
教程文字部分遵循CC BY-NC-SA许可协议。 | ||
|
||
图片部分若无特殊说明,均出自课程资料,使用已获作者同意。 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
# 第零章简介 | ||
|
||
记录一些你在继续阅读之前可能需要了解的信息。 | ||
|
||
如果这是你第一次了解“静态程序分析”,你应该先查看[Github上的简介](https://github.com/RangerNJU/Static-Program-Analysis-Book)。 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,140 @@ | ||
# 初见——静态分析是什么? | ||
|
||
> 静态程序分析是指**不编译**出二进制代码通过测试用例对程序进行测试,仅通过**静态地**分析程序得到程序**不平凡**的性质的过程。 | ||
## 静态程序分析的抽象定义与诠释 | ||
|
||
### 定义 | ||
|
||
> Static analysis analyzes a program P to reason about its behaviors and determines whether it satisfies some properties before running P. | ||
- Does P contain any private information leaks? | ||
- Does P dereference any null pointers? | ||
- 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)? | ||
|
||
即:对一个程序P,静态程序分析在运行P之前分析它的行为并确认它是否满足某些性质。例如: | ||
|
||
- P会导致隐私信息泄漏吗? | ||
- P中会不会有空指针被解引用? | ||
- P中的所有cast操作(掌握JAVA或C++的读者应该熟悉这一操作)都是安全的吗? | ||
- P中的两个指针是否会指向同一个内存地址? | ||
- P中某个特定的断言会失败吗? | ||
- P中的某部分代码是死代码吗? | ||
|
||
### 诠释 | ||
|
||
> Ensure \(or get close to\) soundness, while making good trade-offs between analysis precision and analysis speed. | ||
在分析精度和速度之间做平衡的同时,保证(或近似)soundness。*(对于soundness这个词,有很多种不同的翻译方式,如可靠性、安全性等。)*通常来说,分析的精度要求越高,分析的速度就会越慢。类似的trade-off在计算机世界非常常见。 | ||
|
||
## 静态程序分析的具体解释 | ||
|
||
静态程序分析技术中最重要的两个技术,分别是Abstraction(抽象)和Over-Approximation(过近似) | ||
|
||
### Abstraction | ||
|
||
<img src="../.gitbook/assets/DtoA.png" style="zoom: 50%;" /> | ||
|
||
**抽象是将值从Concrete Domain(具体域)映射到Abstract Domain(抽象域)的过程,也即<u>将具体值映射为抽象值</u>。** | ||
|
||
例如,在上图中: | ||
|
||
- Concrete Domain中变量的值可以是具体的数值,也可能是某种表达式或函数的返回值。 | ||
- Abstract Domain中变量的值分为五类: | ||
1. 正 | ||
2. 负 | ||
3. 零 | ||
4. unknown(未知),通常表达为正的T,读作top | ||
5. undefined(未定),通常表达为上下颠倒的T,读作bottom | ||
|
||
关于unknown和undefined: | ||
|
||
- unknown(未知):根据表达式或函数返回决定,程序运行时会有具体的正负零数值,但运行前只通过该表达式无法确定。如应用C语言中的三目运算符(TODO:加Link)`x = flag ? 1 : -1`中x的值就是unknown的。 | ||
- undefined(未定)程序运行时会遇到错误,并产生未定义行为(TODO:加Link)。如许多语言中divided by zero(除数为零)通常会触发异常/硬件错误,此时如`a=b/0`中a的值就是undefined的。 | ||
|
||
### Over-approximation | ||
|
||
**过近似主要是指对抽象值进行操作时的思想。** | ||
|
||
继续上面的例子,具体来说操作可以分为两类:Data flow(数据流)和Control flow(控制流): | ||
|
||
#### Data flow | ||
|
||
(TODO-加图) | ||
|
||
* 两个正数相加为正数 | ||
* ... | ||
* 正数和负数相加,结果为unknown/top。**这是因为运行前只知道表达式的正负号,无法确定结果是正负零中的任何一个,但程序运行时会有具体的数值。** | ||
* unknown/top除以0,结果为undefined。**这是因为会触发未定义行为。** | ||
|
||
#### Control flow | ||
|
||
在程序执行过程中往往会有分支结构,如果x的值在两个分支中分别被赋抽象正值和抽象负值,那么合并时x抽象值应该是五类中的哪一种呢? | ||
|
||
对于分支合并时的x,**运行前只知道抽象值的正负号,无法确定结果是哪一种,但程序运行时会有具体的数值**。无论是抽象为正还是负都无法准确描述x合并后的状态,所以x合并后的抽象值是unknown/top。 | ||
|
||
## Rice‘s Theorem与静态程序分析目标 | ||
|
||
### Rice's Theorem | ||
|
||
> Any non-trivial property of the behavior of programs in a r.e. language is undecidable. (TODO:加中文) | ||
(TODO:加中文) 这句话中有很多很难的词汇,接下来一一解释: | ||
|
||
* non-trivial properties ~= interesting properties ~= the properties related with run-time behaviors of programs | ||
* r.e. \(recursively enumerable\) 递归可枚举语⾔: recognizable by a Turing-machine | ||
* There is no such approach to determine whether P satisfies such non-trivial properties, i.e., giving exact answer: Yes or No | ||
* 故不存在 perfect \(sound & complete\) static analysis | ||
|
||
### 两个重要概念:Sound与Complete | ||
|
||
> 思考: 作为一个开发者,你使用静态分析器分析自己的代码时,哪种情况更让你觉得糟糕? | ||
> | ||
> * 静态分析器**没有分析出代码错误**的部分。 | ||
> * 静态分析器**判断代码正确的部分为错**的部分。 | ||
Over- and under-approximations are both for safety of analysis. | ||
|
||
sound: 报出所有问题 may analysis: outputs information that may be true \(over-approximation\) \(safe=over\) | ||
|
||
complete: 报出的问题都是对的 must analysis: outputs information that must be true \(under-approximation\) \(safe=under\) | ||
|
||
### 实际应用中静态分析器的设计目标 | ||
|
||
(TODO:加图) **实际应用中往往没有办法做到完美。因而需要妥协。** | ||
|
||
需要静态分析器能在可接受的时间内给出精度满足要求的解。为此: | ||
|
||
妥协 soundness \(false negatives 可能漏报\) | ||
|
||
妥协 completeness \(false positives 可能误报\) \(⼤多数情况的分析,因为 soundness 很重要\) | ||
|
||
## 再讲五块钱的? | ||
|
||
### 关于未定义行为 | ||
|
||
- [未定义行为](https://en.wikipedia.org/wiki/Undefined_behavior)在Wiki上的解释: | ||
|
||
> In computer programming, undefined behavior (UB) is the result of executing a program whose behavior is prescribed to be unpredictable, in the language specification to which the computer code adheres. | ||
- 一个经典的未定义行为例子: | ||
|
||
```c++ | ||
int a[7]; | ||
... | ||
int j = 0; | ||
|
||
//输出结果根据编译器实现不同而不同 | ||
std::cout << a[j++] + a[j] | ||
``` | ||
|
||
### 关于trade-off | ||
|
||
- [存储器层次结构](https://en.wikipedia.org/wiki/Memory_hierarchy):cache-memory-disk-network的经典结构,正是当代计算机设计者们对价格、读写速度和存储容量的典型trade-off。 | ||
- 段页式内存管理:分段和分页方式的存储管理各有其特点,而段页式存储管理将两种方式结合,优缺点互补。 | ||
|
||
### 关于判定问题中经常用到的术语 | ||
|
Oops, something went wrong.