前言

本系列文章源自于南大李老师的软件分析课程，仅作为个人总结。
静态程序分析（static program analysis），是一种方法或者技术用来在执行一个程序之前对该程序的行为和某些感兴趣的属性进行分析的手段。比如判断：1，是否存在私有信息泄露？2，是否存在对空指针的间接引用？3，强制类型转换是否安全？4，两个变量是否可以指向同一块内存？5，断言语句是否成功？6，是否存在死代码需要进行消除？

Static Analysis

Rice’s Theorem

“Any non-trivial property of the behavior of programs in a r.e. language is undecidable.”（r.e. (recursively enumerable) = recognizable by a Turing-machine）–Rice’s Theorem

也就是说，对于那些上面提到的 non-trivial 属性，并不能准确判断程序是否满足这些属性。所以为了得到一些东西，就应该舍弃一些别的东西。

Sound & Complete

假设一个程序存在7处地方和我们感兴趣的某种属性有关，我们想通过静态分析方法找出它们：如果一个静态分析方法具有 Sound 属性时，指的是它常常会报出 N>=7 处结果（绝对包含有正确的7处），在其中有几处地方是我们不感兴趣的，属于静态分析方法判断时产生了失误，称其为误报（false-positive）；如果一个静态分析方法具有 Sound 属性时，指的是它常常会报出 N<=7 处结果（是正确的7处的子集），这N处地方都是我们想要的结果，但是还有几处地方静态分析并没有找到，这也属于静态分析方法判断时产生了失误，称其为漏报（false-negative）。前者称其为过近似（Over-approximate），后者称之为 Under-approximate。
一般采用的静态分析方法都是牺牲掉 Complete ,保留 Sound 。这样得到结果虽然会有误报，但是这个结果中包含有所有的正确结果。即 Sound but not fully-precise static analysis 。

Sound 示例

对于下面的代码：其中类 B 和 C 是 A 的子类，代码中有两条路径可以到达 B b’ = (B) a.fld;
对于 UnSound 的情况下，只会判断某一条路径（取决具体实现）比如仅仅判断蓝色路径，认为这段代码是正确的。而在 Sound 的情况下，是要对两条路径都要进行判断的，因为不确定程序执行流具体会走哪条路径，对蓝色路径判断的结果为正确，对绿色路径判断的结果为错误，对于语句 B b’ = (B) a.fld; 是否能够执行成功并不能得到一个确切的结论。我们认为前者得到的结论是不安全的，而后者得到的结论是安全的。

在静态分析中，下面的代码执行完毕之后 a 的值为多少？

 if(input)a=1;elsea=0;

答案是 a=1 or a=0，也可以精确的描述为：当 input 为真时，a=1；input 为假时，a=0。

小结

Static Analysis: ensure (or get close to) soundness, while making good trade-offs between analysis precision and analysis speed.

抽象和过近似（Abstraction + Over-approximate）

静态分析示例

问题：判断对于某个给定的程序中所有变量的符号。（+、- 或者 0）

下面分两步来描述静态分析处理该问题的步骤：

抽象

即对程序中出现的具体的值进行抽象。如下所示：左侧为具体的语句，右侧为抽象的结果

      v=10；       那么 v 对应的符号为正(+)。
      v=-9；        那么 v 对应的符号为负(-)。
      v=0；         那么 v 对应的符号为0(O)。
      v=e?1:-1；那么 v 对应的符号为不知道(T)。（不清楚 e 的值为真或假）
      v=e/0；      那么 v 对应的符号为未定义(⊥)。（除0是一个未定义的运算）

过近似

在将程序中的语句抽象完之后，然后在抽象后的结果上进行过近似操作

转换函数（Transfer Functions）

转换函数是定义如何在抽象值上对不同的程序语句进行评估，至于评估什么要根据程序中语句的语义和我们要分析的问题来决定。接下来以下面这个图片进行说明：

左侧是转换函数，或者说是转换公式会更加确切点。包括有正数+负数=不知道；任何数/0=未定义等等。转换函数所表示的意义并不难理解。

右侧是一个程序中存在的具体语句，注意：对变量符号的判断是在已经抽象的基础上进行的。最后得到了三处未定义的地方，第一处为除0，第二处的数组下标为负值，第三处的数组下标可能为负值。其中第三处的未定义是误报，因为在程序的具体执行中，我们可以轻易的计算出 a 的值为9，在实际执行中并不是负值，即语句是正确的。

控制流处理（Control Flow handling）

控制流处理通常处理：在程序存在分支的情况下，汇合点处变量的符号如何来判断。
如上图所示：左边是具体的语句，从语句 x = 1 ; 开始程序进入到两个不同的路径里面，分支的汇合点为语句 z = x + y ; 。可以看到左边路径得到的y为正，而右边路径得到的y为负，那么得到汇合点处变量y的值为不确定(T)。

总结

这一部分简单介绍了静态分析的特点比如：不需要执行程序，总是需要保持 Sound 及其原因，保持 Sound 的结果导致容易产生误报。以及静态分析处理程序的两个重要步骤：抽象和过近似。后面会介绍静态分析中 IR 的生成和 CFG 的建建立。未完待续~

静态程序分析chapter1 - 概述和两个重要步骤相关推荐

静态程序分析chapter3 - 数据流分析详述（Reaching Definitions、Live Variables、Available Expressions Analysis）
文章目录二. 数据流分析 introduction1 introduction2 输入和输出状态转换函数数据流分析应用 1,Reaching Definitions Analysis 概述用途 ...
静态程序分析（一）—— 大纲思维导图与内容介绍
本系列文章为,基于奥尔胡斯大学的Anders Møller 和 Michael I. Schwartzbach两位教授于2022年2月1日所出版的<static program analysis ...
静态程序分析chapter5 - 常量传播分析上（Costant Propagation Analysis）
四. 数据流分析之常量传播(Constant Propagation) 概述 Constant Propagation:Given a variable x at program point p, d ...
静态程序分析chapter4 - 基于格（Lattice）理论的数据流分析
文章目录三. 格理论函数不动点偏序(Partial Order) 上界和下界最小上界和最大下界 glb 和 lub的属性格(lattice).半格.完备格.乘积格数据流分析框架单调性和不 ...
静态程序分析chapter2 - IR（Jimple）和 CFG
文章目录一. IR(Intermediate Representation) 编译器(Compiler) 3AC(3-Address Code) Soot和它的IR:Jimple JVM中的方法调用 ...
【软件分析/静态程序分析学习笔记】7.指针分析(Pointer Analysis)入门
写在前面的话本渣有幸成为南京大学软件学院研究生,在前往仙林校区蹭课的时候偶然发现了这门宝藏课程,听了以后感觉深有收获,但又因为课程难度较大,国庆假期归来发现遗忘较多,因此开了一坑来记录自己对每节课知 ...
【软件分析/静态程序分析学习笔记】2.中间表示(Intermediate Representation)
写在前面的话本渣有幸成为南京大学软件学院研究生,在前往仙林校区蹭课的时候偶然发现了这门宝藏课程,听了以后感觉深有收获,但又因为课程难度较大,国庆假期归来发现遗忘较多,因此开了一坑来记录自己对每节课知 ...
程序崩溃分析工具_程序分析工具| 软件工程
程序崩溃分析工具 A program analysis tool implies an automatic tool that takes the source code or the execut ...
搞懂静态代码分析，看这文就够了！
作者 | 赖建新来源 | 鉴释封图 | 东方IC 什么是静态代码分析? 静态代码分析是指在不实际执行程序的情况下,对代码语义和行为进行分析,由此找出程序中由于错误的编码导致异常的程序语义或未定义的 ...

静态程序分析chapter1 - 概述和两个重要步骤

文章目录

前言