中国建设部网站-玻璃幕墙,企业网站建设服务电话,建设银行手机网站,给人家做的网站想改怎么改#x1f517; 课程链接#xff1a;李樾老师和谭天老师的#xff1a;南京大学《软件分析》课程01#xff08;Introduction#xff09;_哔哩哔哩_bilibili 目录
一、静态程序分析介绍
1.1 PL and Static Analysis 程序语言和静态分析
1.2 为什么要学 Static Analysis?
… 课程链接李樾老师和谭天老师的南京大学《软件分析》课程01Introduction_哔哩哔哩_bilibili 目录
一、静态程序分析介绍
1.1 PL and Static Analysis 程序语言和静态分析
1.2 为什么要学 Static Analysis?
1.3 什么是静态分析 ?
1.4 静态分析的特征和例子
1.4.1 sound and complete no perfect static analysis
1.4.2 false negatives or false positives (useful static analysis)
1.4.3 Static Analysis 例子 — Birds Eye View
1.5 静态分析大致步骤—举个例子
1.5.1 Abstraction抽象
1.5.2 Over-approximation(近似): Transfer Functions转换函数
1.5.3 Over-approximation(近似): Control Flow控制流
1.5.4 总结 一、静态程序分析介绍
1.1 PL and Static Analysis 程序语言和静态分析 PL (Programming Languages, 程序语言) Static Analysis静态分析 如下图所示PL可以分为三个主题理论、环境和应用
理论语言设计、语言的类型系统、形式语义和逻辑……环境编译、运行时系统……应用程序分析、程序验证、程序合成…… 程序语言的分类 命令形语言C、Java 函数式语言JavaScript、 逻辑式语言一条条逻辑声明出来的语言
挑战 这么多年来语言的核心没有变但是软件越来越复杂如何保证大规模复杂程序的安全性、可靠性…… 1.2 为什么要学 Static Analysis?
从代码层面来看静态分析可以做很多事情后续也会详细讲到
对程序可靠性Program Reliability 空指针引用 null pointer dereference 内存泄漏 memory leak……对安全性 Program Security 私有信息泄露 private infomation leak, 注入攻击injection attack……编译优化 Compiler Optimization 死代码消除 Dead code eliminationcode motion……程序理解 Program Understanding IDE call hierarchy, type indication……
对于程序员静态分析可以帮助写更高质量的代码。 1.3 什么是静态分析 ? Static analysis analyzes a program P to reason about its behaviors and determines whether it satisfies some properties before running P. 静态分析(static analysis) 是在程序运行之前分析其行为确定它是是否能满足某些特性要求
有没有一些程序泄露有没有空指针引用异常?所有的变量variable 用之前都初始化了吗所有的cast operation是安全的吗v1和v2会不会指向相同的内存地址程序中的断言语句 assert 会失败吗死代码……
但是根据Rice Theorem大米定理/莱斯定理不存在一个方法可以给出一个确切的答案Yes or No原文如下 Any non-trivial property of the behavior ofprograms in a r.e.language is undecidable. 这句话里的一些词
r.e.(recursively enumerable) recognizable by a Turing-machiner.e. language: 递归可枚举的语言图灵机可识别的语言可以理解为现代的编程语言C 、JAVAnon-trivial property≈ 一些有趣/有价值的性质 ≈ 与动态运行时行为runtime behaviors相关的性质就像前边列举的空指针、内存变量什么的。undecidable: 给不出确切答案
可以这么理解 一个递归可枚举的语言图灵机可识别的语言可以理解为现代的编程语言C 、JAVA他的一些non-trivail property与程序运行时行为相关的性质例如是否有空指针、有没有内存泄漏是不能确定的例如不能准确地说有空指针或者没有。
再学术一点的理解 一个 完美的静态分析(perfect static analysis) 是满足 sound and complete 的sound 和 comlete是 静态分析的两个特征见1.4.1. 大米定理就是在告诉我们不存在完美的静态分析可以准确地回答Truth也就是不能同时满足sound 和 complete. 1.4 静态分析的特征和例子 为什么没有一个perfect的呢因为一些情况其实不可避免导致分析要么太“过”(sound)要么太“保守”(complete)。 1.4.1 sound and complete no perfect static analysis 如图所示complete和sound的关系
truth是这个程序中理论上的所有的正确的答案complete指的是报出来的都是对的但是不全sound包含了所有正确答案
1.4.2 false negatives or false positives (useful static analysis) 既然没有perfect静态分析为什么还要去研究呢因为可以对一方妥协由此就有了useful static analysis有用的静态分析。 Useful static analysis
Compromise soundness (false negatives假阴性) : 妥协soundness就是不sound会产生漏报错的没检测到Compromise completeness(false positives假阳性)妥协completeness不complete会产生误报对的说是错的
在绝大Useful静态分析中我们所研究的更多是妥协completeness要求分析是 Sound 的虽然并不全都准确not fully-precise宁可错杀100不可放过一个可以误报但是不能漏。
soundness越好分析就越好。
1.4.3 Static Analysis 例子 — Birds Eye View 如下图对左侧的代码进行分析的时候产生的2个分析结果 这两个分析结果都是对的没有产生漏报都满足sound且 1 更准确但是昂贵 2 不够准确但是cheep; 还有一些可能的分析结果如下: 3. x 0, 1, 2, 3, 4 4. x 1, 2, 3, 4 其中3产生了误报都是涵盖了所有情况也是sound是对的都是4漏了0是错误的。
一句话概括静态分析 静态分析是在确保or 尽量接近soundness的同时在分析精度(precision)和速度(speed)之间做一个平衡这才是一个Useful 静态分析 在实际分析中可能不存在真正的soundness的例如java的反射机制、Java的动态类机制都会影响到soundness所以是“尽量接近”soundness。 1.5 静态分析大致步骤—举个例子 从技术层面分析静态分析的大致步骤用两个词来总结静态分析 Static Analysis Abstraction Over-approximation 以下通过一个例子来初步感受一下静态分析 例如要给一个程序的所有变量判断正负0-需要以下两步
AbstractionOver-approximation Transfer functionsControl flows
1.5.1 Abstraction抽象 抽象就是把具体的域值映射到抽象域里。 如下图将左边的变量映射到右边不同的正负情况。抽象成不同的符号。 (unknown)如果当前数值会因为变量改变而呈现为不同的状态 (undefined): 经过判断肯定不符合int定义的例如一个除以0的数或者字符等。
1.5.2 Over-approximation(近似): Transfer Functions转换函数 在完成抽象之后我们需要做的就是近似其中一部就是用到转换函数转换函数的作用可以概括为如下两句 在静态分析中转换函数定义了一种转换规则如何评估关于抽象值的不同程序语句根据“要分析的问题/目标”和不同程序中的“语义semantics”来进行评估。 针对于这个例子要分析的问题转换的规则如下图所示 利用以上规则来评估一下具体的程序语句如下 对于变量c我们找到了一个除以零的错误对于变量py是负数我们找到了一个负数索引的错误对于变量q因为a不确定是否为负数而判定其为undefined但其实a并不是负数这里就是一个误报 通过判断符号我们成功找到了两个错误 c 和 p说明静态分析是很有用的useful但是Over-approximation 的静态分析也产生了误报 假阳性 false positives。
1.5.3 Over-approximation(近似): Control Flow控制流 近似还要有控制流也就是程序执行的流要将所有流汇聚的地方进行合并抽象 flow merging。 如下图左侧的程序片段转为右侧的控制流然后判断符号[ z x y ] 是汇聚的点所以要枚举其所有分支进行合并即 [ y ] 在静态分析中如果程序很复杂我们无法在实际应用中枚举所有的路径分支流合flow merging 作为over-approximation 的一种方式是常用的分支推断技术提升了Soundness也降低了Completeness也导致了不可避免的误报问题。
1.5.4 总结 抽象就是将具体值转为符号值。因为在Abstraction抽象过程中进行了值域空间的 降维抽象 所以在转换函数映射中静态符号执行和动态实际实行的结果之间是存在差异的这是不可避免的。 近似就是将每个语句和每个语句之间的关联进行抽象化为图来说就是每个节点和每个节点之间的箭头 · transfer funtions 是对每个语句的近似 · control flow 的近似就是 每个箭头 的近似 将每个语句以及不同语句之间的箭头 都进行近似就实现了对整个程序的近似。
