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

Tattoo

发布日期: 2020-07-08 13:04:40 浏览量: 57
评分:
star star star star star star star star star star_border
*转载请注明来自write-bug.com

最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)
原作者:bsauce
原文链接:https://www.jianshu.com/p/8d06766d232c

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

推送门南大课件 南大视频课程 北大课件

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

讲数据流分析的时候,关键是首先抽象表示数据(一般是用向量),然后设计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,他们之间的关系可以用一个图很好的表示。

  • sound表示报告包含了所有的真实错误,但可能包含了误报的错误,导致误报

  • complete表示报告包含的错误都是真实的错误,但可能并未包含全部的错误,造成了漏报

3.软件分析步骤

  • abstraction:抽象值,定义集合(类别)

  • Safe-approximation安全近似

    • Transfer Functions:对抽象值的操作,转换规则
    • Control flows
上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

79
文章数
34
评论数
eject