【课程笔记】南大软件分析课程1——课程介绍

roger

侵权删。

首先非常感谢南京大学李樾[1]和谭添[2]老师的无私分享，之前学习程序分析是看的北大熊英飞老师的ppt，但是很多地方没看懂，正如李樾老师所说的那样，熊英飞老师的授课涵盖非常广，不听课只看ppt的话，理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂，示例都是精心挑选的，所以墙裂推荐。

推送门：南大课件[3] 南大视频课程[4] 北大课件[5]

我觉得上这门课，最大的收获就是，锻炼出一种软件分析的程序化思维。之所以做这个笔记，是为了总结和方便回看，毕竟回看笔记比回看视频快很多。

讲数据流分析的时候，关键是首先抽象表示数据（一般是用向量），然后设计transfer function转换规则和control flow控制流规则，然后遍历基本块，根据这两个规则去计算，一旦某个基本块的抽象表示改变了，则再次遍历一遍。这对于我们以后设计数据流分析算法是很有帮助的，我们需要思考所要解决的问题到底是forward还是backward，是may还是must analysis，这相当于是一个分析模板。

本课程主要内容：IR，数据流分析，过程间分析，CFL可达性和IFDS，指针分析，抽象解释。

1.PL—Programming Languages

理论：语言设计，类型系统，语义和逻辑

环境：编译器，运行系统

应用：程序分析，程序验证，程序合成

技术：抽象解释（Abstract interpretation），数据流分析（Data-flow analysis, ），Hoare logic，Model checking，Symbolic execution等等

静态分析作用：程序可靠性、程序安全性、编译优化、程序理解（调用关系、类型识别）。

2.soundness与completeness

soundness：对程序进行了over-approximate过拟合，不会漏报（有false positives误报）。

completeness：对程序进行了under-approximate欠拟合，不会误报（有false negatives漏报）。

很多重要领域如军工、航天领域，我们追求的是soundness，但是要平衡精度和速度。那么我们绝大多数软件分析方法都做到了completeness，那么只要能证明满足soundness，那么该分析方法就是正确的。

那么什么样的SA是完美的呢？定义是既overapproximate又underapproximate的SA是完美的。overapproximate也叫sound，underapproximate也叫complete，他们之间的关系可以用一个图很好的表示

【课程笔记】南大软件分析课程1——课程介绍

0-1-sound_complete.png

complete表示报告包含的错误都是真实的错误，但可能并未包含全部的错误，造成了漏报；sound表示报告包含了所有的真实错误，但可能包含了误报的错误，导致误报。

3.数据流分析步骤

1.abstraction：抽象值，定义集合（类别）2.Safe-approximation安全近似·Transfer Functions：对抽象值的操作，转换规则·Control flows

参考：

南大课件[6]

南大视频课程[7]

北大课件[8]

References

[1] 李樾: https://yuelee.bitbucket.io/index.html[2] 谭添: https://silverbullettt.bitbucket.io/[3] 南大课件: https://pascal-group.bitbucket.io/teaching.html[4] 南大视频课程: https://zhuanlan.zhihu.com/p/110050716[5] 北大课件: https://xiongyingfei.github.io/SA/2019/main.htm[6] 南大课件: https://pascal-group.bitbucket.io/teaching.html[7] 南大视频课程: https://zhuanlan.zhihu.com/p/110050716[8] 北大课件: https://xiongyingfei.github.io/SA/2019/main.htm

---