侵权删。 首先非常感谢南京大学李樾[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与completenesssoundness:对程序进行了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.pngcomplete表示报告包含的错误都是真实的错误,但可能并未包含全部的错误,造成了漏报;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
|