程序分析理论(引论)

robots

 

前言 Preface

本文是关于设计静态分析程序的前置基础理论系列介绍的第一章 引入和介绍

 

介绍 Introduction

为什么要代码分析 Why Program Analysis

不同于渗透测试的代码分析,本文的代码分析是程序开发流程中的一个重要环节。本文的代码分析包含两种基本思路:一种是遍历所有路径 一种是语义分析。基于第一种思路,我们能在确保程序能够正常运行的同时获取所有可能的输出结果从而在程序使用过程中将输出控制在这些已知正常的结果之中,达到程序能够可控安全。基于第二种思路,我们能够利用程序低成本高效率的实现通过分析语义证明代码安全性。

代码分析能做什么 What Can Program Analysis Do

首先,我们要确认的是代码分析是否是完美的。是否存在写出一种代码分析程序能够适用于证明任何程序的安全性。答案是不能。以经典的停止问题作为说明,我们不能成功编写一个程序对所有的程序和输出的停止问题做出响应。正如我们不能判定SQL注入是由不受信任的输入构造的吗,指针被释放后是否被解除引用。当分析器发现错误时,程序停止,如果没有你们就继续运行。但是正是因为存在不可判定的问题,导致分析器无法准确判断安全性。这就出现了误报,漏报的现象

虽然,完美的代码分析程序不存在,但是有用的代码分析程序是可能的。有用的代码分析是在可靠性和完整性之间选择最好的位置实现最少的误报和漏报。可靠性指分析为真则为真,完整性指因为是真所以分析为真。所以代码分析能做的是面对不同需求选择最佳方案以满足需求。

不同代码分析方法的共性 The Nature of Program Analysis

1.在所有的方法中,为了保持可计算性,我们只能提供近似解。 in order to remain computable one can only provide approximate answers

以下面代码为例:

S 是不包含y的一系列操作,我们可以清楚的知道,y的最后可能是1或者2.假设y只能是1,即x>0或者在x<=0 y=1 时,S会使程序崩溃。但是,现实是我们不能准确判断S 的情况,那么我们倾向于将1和2都考虑进去,也就是创建一个更大的输出集合,即使某些输出永远不会实现。这就是为了可计算性提供近似解。

2.所有方法都要包含语义分析 all methods should include semantic analysis

语义分析在于将所有用户可控的输入作为被污染的数据,将代码本身的数据作为没有被污染的数据。原则就是如果一个函数的参数可以是被污染的数据,那么参数也一定可以是未被污染的数据。但是,如果一个函数的参数只能是未被污染的数据,那么如果参数是被污染的数据,就会可能引起危险。

语义分析实现步骤:1. 定义所有变量为污染或者是未被污染 2. 对所有赋值语句进行转换 即x = y 转义成 污染参数 = 未被污染的参数 或者 未被污染的参数 = 被污染的参数 3. 依据污染 = 未污染 合法,未污染 = 污染 非法 判断程序是否安全

针对一些特殊的语法结构 如(if else / for之类的结构)我们有两种做法:

  1. 基于语句的分析,即把所有可能性列出来,一一判断
  2. 基于方法的分析,把每一个特殊结构单独分析,最后整合在一起

一个例子 An Example

以while循环为例。while通常会是一系列语句包括判断,执行,循环。那么我们可以把执行的赋值语句当作一个模块,判断和循环当作另一个模块。那么我们要对语法进行分类。其中包括算术运算,逻辑运算,赋值运算。同时运算符也是这么分类。随后对参数进行分类。包括变量,常量。除此之外,我们还要给每一个语句一个标签。使得我们对于while循环语句可以进行简单的描述。

接下来我们以下面代码作为演示

Table1

我们可以看见一系列形如[ y := x ]的表达式。这是对赋值运算的描述,右上角的数字属于语句的标签。一个完整语句用 ; 结尾。同时我们还用( )对块语句进行包裹以解决歧义。此外,[ y > 1 ]是逻辑运算的描述。这样的描述方式可以让我们识别程序的基本架构,同时又不需要画出流程图

上述表达虽然具有逻辑性但是依旧无法直观对数据进行分析,所以我们做出如下图的表格作为补充

Table2

我们可以看到表格最上方一行 l RDentry(l) RDexit(l) 分别表示为我们给予语句的标签,进入该语句时所有的数据信息,退出该语句时所有的数据信息。左侧一列为标签,表格中一系列形如 (x,4) 的表达式的原型可以写作 (v,l) ,即 一个变量,和该变量的赋值语句的标签。我们可以看到最初标签都是 ? 即该变量的赋值语句并没有在我们描述的这一段代码中。同时,我们可以看到同一行中会出现多个同一个变量的表达式(如表格内第三行(z,2) (z,4))这是由于本文上面提到的代码分析的共性中的为了保持可计算性只提供近似解。我们可以看到Table1 中关于z的赋值语句有两条,分别是2和4 这也正对应表格内的(z,2) (z,4)。我们无法判断运行过程中是否会执行4语句,所以我们将2和4 都包含在可能的表中。

以上就是引入部分的全部内容,如果有任何不对的地方请与我联系。

作者:DR@03@星盟

(完)