class 1 介绍
逛b站的时候,发现南京大学开设了软件分析课,和我目前学的课程有很大的重合。由于学校开的网课没有好好听,打算好好做人跟着南大的老师学一下静态分析课的内容。
ps:由于我的笔记是用Typora上写,写完再上传的,所以格式会有点问题,请见谅;并且笔记里面可能会有表述、语病等方面的问题。
严格来说,静态分析就是属于程序语言的研究领域,并且是应用部分
-
程序语言
-
理论部分
(1)语言设计
(2)类型系统
(3)语义、逻辑等。。。。
-
环境:就是让语言跑起来
(1)编译器
(2)运行系统
-
应用:程序是否能正常运行、是否合理等的证明
(1)程序分析
(2)程序验证
(3)程序合成
命令式语言:C、C++、Java(就是命令计算机一步一步执行)
函数式语言:JavaScript
逻辑式语言:
目前的发展:语言内核没有改变,但是程序变得越复杂和庞大。
=>所以,如何保证程序的可靠性、安全性等。所以程序分析的使用很重要
-
-
静态分析的应用
- 程序的可靠性:eg:空指针、内存溢出的检查
- 程序的安全性:个人信息泄漏、黑客
- 编译优化:会将坏的程序进行优化,eg:永远不执行的程序会被删除、重复的语句进行简化
- 程序理解:eg:IDE中调用的提示,类型指示,vscode里面点击函数就能知道它的定义位置、知道它在哪边被调用。
-
静态分析的定义
在运行程序P之前,分析该程序的行为和性质是否能满足
eg:看程序是否会造成信息泄漏,是否有空指针,类型转换是否满足,指针是否指向同一个地址(临界区是否有竞争),assert是否会fail,程序块是否是死代码是否可以去掉。
=> 但是,莱斯定理说,对于递归可枚举语言(r.e语言,就是目前所有语言)的所有非平凡性质(non-trivial,所有有价值的、程序运行时的行为相关的,之前举例都是non-trivial)都是不可判定(undecidable)的
-
静态分析的关键属于
对于一个完美的静态分析器,是既sound又complete
但是,根据莱斯定理是不存在的
sound:是包含所有的错误,但是也存在误报 =>报错比实际多
complete:是提出的所有错误都是真的错误,但是存在漏报=> 报错比实际少
漏报(假阴性,是阳性但是认为阴性,阴性就是没有病),误报(假阳性,没有阳性却变成阳性)在静态分析中,追求sound,因为错误都包括了。
-
实际运行中,判断:
静态分析就是程序在运行前的判断,所以两种可能均存在。
第一个比较准确,但是代价太大了,需要知道上下文,时间和空间消耗大;
第二个不准确,但是代价小;
第三个也是soundness
第四个由于缺少0,所以不soundness。
所以,静态分析的研究目的,必须保证sound的前提下,平衡速度和准确度的关系。
静态分析:抽象+过拟合(过近似)
-
抽象
将程序中具体的值抽象为符号(+,-,0,⊥undefined,┬unknown)
-
过近似(over-approximate)
-
转换函数:将程序每个语句都变成抽象值(就是规定转换规则)
-
根据分析目标、语句的语义来定义转换函数
转换规则:
举例:
-
-
控制流图
将所有语句的执行抽象为控制流图,然后将所有变量抽象为符号,就构成了。