(二)数据流分析基础

区块链安全 1年前 (2022) admin
442 0 0
(二)数据流分析基础

上一篇文章:(一)初识软件分析

下一篇文章:(三)Datalog 和程序分析

数据流分析

基本思想:程序视作状态和状态的转移两部分组成,忽视状态转移的条件,分析状态转移时的变化。

近似的两种方案:

  1. 忽略程序的条件判断,认为程序的所有分支都有可能到达
  2. 控制流分叉合并。这会大大的减少计算量。

这些性质在后面会解释。

符号分析

思想:对变量进行抽象,分析输入的符号和输出的符号,得到抽象的结果。在此基础上可自定义分类和类似地拓展,用更加抽象和概括的符号。例如,对于整数类型,我们可以分成零、正、负、未知四种输入和结果,而不考虑具体的数值。

按照状态转移,我们可能有多条执行路径能够到达目的点 A。例如,if 语句是典型的区分执行路径的的方式。由于未知结果的函数 func1func2,a 最终的符号可能是正、负或者未知。那么,我们可以得到 2 条可能的执行路径(0、5、1、未知)或者执行路径(0、-1、1、 未知)。这里也体现了忽视条件判断的观点。

1
2
3
4
5
6
7
8
9
10
11
int a = 0;
a = func1();
b = func2();
//位置1
if(a > 5){
    a -= 4;
} else {
    a = 1;
}
//位置2
a = b;

我们可以:

  1. 进一步抽象,合并数据,将第二步的 5 和 -1 抽象为 “非 0 数”。
  2. 在控制流汇合的部分,如 if 执行完后,合并数据,而不是单独视作单独的数据流。

例如,当经过了 if-else 语句之后,a 的值至少是 1,所以可以合并后 a 的值变化是(0,未知,大于 0,未知)

最后,总结一般流程:

  1. 确定状态集合:
    S={(a1,a2,a3,…)|ai∈D}

    D 是每个子状态或者元素的定义域。

  2. 每个执行路径上的每个节点视作状态集合 S 的元素。
  3. 确定初始值状态 DATAentry,设置执行路径上每个节点的状态默认值 DATAnode=(T,T,T,⋯)T 表示任何情况,随后的半格理论中会再次说明。
  4. 确定节点的状态转换函数 fv:S→S,具体的函数规则由每个节点的内容决定。
  5. 在控制流汇合处,例如在节点 v 处回合,确定交汇运算 MEETv=Πw∈pred(v)DATAw,其中 v 表示当前节点,pred(v) 表示当前节点的前驱节点的集合,所以 w 指的是前驱节点。我们约定,交汇处会覆盖默认值,也即 aiΠT=aiΠ 表示交汇运算。
  6. 如果数据流中某个节点的前驱节点更新了,那么更新该节点。
  7. 如果没有任何节点的状态更新,那么结束执行。

如果需要深入探讨这个基本流程的性质,一般会包括以下内容:

  • Terminating 终止性。符号分析是否会终止,还是一直循环。
  • Confluent 合流。这指的是更新节点时的顺序是否会影响到最终的结果。

以上两者可以笼统的归纳为符号执行方法是否收敛 (Convergence),这将会涉及数理逻辑中形式系统的知识。

活跃变量分析

Liveness analyze 活跃变量分析在编译器、垃圾回收机制中非常常见。对于给定的程序,对于语句 S,变量 V 定义在语句 S 之前,如果 V 的值在执行 S 语句之后还会被读取,那么 V 就是活跃变量。这里需要额外注意的是,活跃变量并不是根据变量名来区分的,而是根据变量实际代表的对象(例如指针指向的值)来区分变量。

1
2
3
4
5
6
7
8
9
10
var x,y,z;
x = input;
while (x>1) {
y = x/2;
if (y>3) x = x-y;
z = x-4;
if (z>0) x = x/2;
z = z-1;
}
output x;

例如第四行的变量 y 被覆盖了,那么指向第四行之前的变量 y 和执行第四行之和的变量 y,是不同的变量,而且在 y 的值变化的过程中,原来的 y 没有被读取。所以在第一行确定的变量 y 不是活跃变量。

但是第 9 行的变量 z,是活跃变量,尽管它被覆盖了,但是在覆盖之前读取了 z 的值。

活跃变量的分析属于 may 分析,归纳为活跃变量的变量,在后续的执行中可能就不是活跃变量了,因此,一般从程序结束的出口开始分析活跃变量

(二)数据流分析基础

对于执行路径的每个节点,我们给出每个节点活跃变量的集合 ,然后从出口倒着向入口分析,在不同控制流的交汇处取并集,这样就可以得到满足 “变量在当前语句之和会被读取” 的性质。

最后总结一般流程:

  1. 初始化出口处的活跃变量为空 DATAV={}
  2. 定义从后往前时每个节点的活跃变量的转换函数

     

    被覆盖被重定义被读取fv(L)=(L−KILLv)∪GENvs.t.{KILLv={x|x被覆盖 or x被重定义}GENv={x|x被读取}

     

    其中 L 表示当前节点从后继节点获取的活跃变量的集合,KILLv 是需要在活跃变量集合中删除的变量,GENv是当前节点 v 处产生的新的活跃变量。

  3. 交汇处运算 MEETV=⋃w∈succ(v)DATAw,表示后继节点的状态的并集。
  4. 更新活跃变量集合 Lv=fv(MEETv)
  5. 如果某个结点的后继结点发生了变化,则使用结点更新运算更新该结点的值。
  6. 如果没有任何结点的值发生变化,则程序终止。

活跃变量分析需要考虑 soundConvergence,也即严格满足 may 分析,活跃变量集合包含所有可能的活跃变量;活跃变量分析的算法需要收敛。

单调框架

为了确保符号分析和活跃变量分析的收敛性和正确性,提出了数据流分析的单调框架,通过一个通用的可定义的框架,囊括数据流分析基本流程,并且检验每一步的状态转换函数和参数。一般而言,单调框架会涉及到

  • 设置节点对应的不同类型集合的统一接口。
  • 设置节点转换函数的统一接口。

在开始之前,读者需要明白以下数学内容。

格理论基础简介

(Lattice)是其非空有限子集都有一个上确界(称为)和一个下确界(称为交)的偏序集合(poset)。如果学习过离散数学,那么知道偏序关系是对于 “大于” 或者 “小于” 关系的抽象。

先复习二元关系性质的内容,R(x, y) 表示 x, y 满足关系 R

  • 自反性。对于集合 X 上的二元关系 R,若满足:取 X 里任一元素 a,且满足对于所有 a 皆存在 (a,a) 在 R 集合中,则称二元关系 R 是自反的,或称 R 具有自反性,或称 R 为自反关系。例如 a >= a。
  • 反自反性。若集合 X 上的二元关系为非对称关系,则

 

a,b∈X,(a,b)∈R⟹(b,a)∉R

 

例如 a>b,那么就不会有 b>a。

  • 对称性。若集合 x 上的二元关系为非对称关系,则对于所有(a,b)R(b,a)R
  • 传递性。数学上表示为:
    ∀a,b,c∈X, aRb∧bRc⇒aRc

    例如:大于等于具有传递关系:若 a⩾bb⩾cb⩾c 

半格 semilattice

(二)数据流分析基础如果理解了「群、环、域」这些近世代数的基本内容,可以很容易的理解这些抽象定义。我们开始理解格和数据流分析的关系。在前面经常提到「抽象」这个词,比如对于具体的符号 +-,在某个节点中可能同时出现,那么用更加抽象的符号T 表示。其实,这里的 T 相当于格中的最大元。每一步的抽象类似于偏序关系,构造不同抽象层次的符号集。

半格的高度:偏序图的层次数,也等同于半格的偏序图中任意两个结点的最大距离+1。例如下面的偏序图,半格高度为 3

(二)数据流分析基础

单调框架的基本流程

在有了以上的知识后,我们给出概括性的基本流程:

  1. 构建控制流图 (V, E)。请回忆前面我们规定每个语句处视作状态,状态用节点表示,状态之间的联系用节点之间的边表示。
  2. 一个有限高度的半格(?,⊓)。「有限」表示控制流会终止,也表示数据流分析收敛。S 表示状态的集合,例如判断数值正负的符号集合,那么 S 包括 {+, -, T}。⊓ 则定义了控制语句交汇处状态汇总的规则。
  3. 一个 entry 的初值 Ientry 表示初始输入,不同的输入,程序的收敛性和正确性可能不一样。
  4. 一组单调的节点转换函数,对除了入口的任意节点 v∈V−entry 存在一个 单调函数 fv。除了初始输入,我们对于每个状态的抽象层次(例如上面提到的 零 正 负和 T。大于表示超集),使用偏序关系进行排序。采用单调函数以保证偏序关系。

下面是伪代码实现:

(二)数据流分析基础
  1. 程序入口赋初值为 I
  2. 除了初始位置的其他节点都赋予默认值 T
  3. 初始化未访问的节点集合
  4. 如果未访问的节点数量大于 0,那么
    1. 从未访问的节点中选取一个节点 v
    2. 在未访问节点集合中删除节点 v
    3. 交汇节点 v 的每个前驱节点 w, 确定交汇操作。
    4. 如果节点交汇操作输入到节点 v 的状态转移函数后,导致节点 v 的值之前值不同,则更新他的后继节点。
    5. 覆盖节点 v 原来的状态

从上面的流程可以看出来,选取的开始的节点,并不是从初始输入的程序入口处开始执行,这其实是出于考虑状态转换时可能存在特殊的节点,执行到它们后,根据前面提到的规则,可能无法向前驱节点传递状态改变。

小结

(二)数据流分析基础

数据流分析的性质

最大下界

这一般会在离散数学中学习,在偏序集合中(允许大于等于),对于某个子集的最大下界,是所有不大于它的元素中的最大元。如下图举例(默认读者理解哈斯图):如果找 d, e 的最大下界,d,e 的下界有 a,b,c。然后找 a, b, c 中的最大元,由于 a, b, c 没有最大元,所以不存在最大下界。但是如果找 {d, e, b} 最大下界,可以明显的知道是 b。

(二)数据流分析基础严格定义可以参考下图:

(二)数据流分析基础可以看出,半格是特殊的偏序关系,所有元素都存在“大小关系”。

数据流分析的安全性

安全性体现为保持 sound,也就是不会出现 false positive 但是可能出现 false negative。交汇的操作后的值会比单独的每一条路径在此节点的值更小。这里嵌套的状态转移函数表示从入口到节点 Vi 的状态转移过程。严格的定义如下:

(二)数据流分析基础如果考虑到路径上的节点其实也可能进行了交汇操作,上面的结论是否还是成立呢?其实只要满足前面小节中变化函数是单调函数,而且交汇函数形成半格即可。详细说明如下:

(二)数据流分析基础

数据流分析的分配性

分配性是为了克服 false negative 提出的。分配性的定义:一个数据流分析满足分配性,如果

 

∀v∈V,x,y∈S:fv(x)⊓fv(y)=fv(x⊓y)

 

可以发现,安全性可以理解为右边小于等于左边。可以通过集合运算验证是否满足分配性,注意观察下面的结果是等号而不是被包含,另外要理解即使满足了分配性,数据流分析可能还是近似的,因为节点的状态转换函数还是可能是近似的。我们略过证明过程。

(二)数据流分析基础

数据流分析的收敛性

由于数据流分析的基本原理是交汇操作和节点转换函数,再结合基本条件中节点转换函数必须是单调的,因此随着路径地加深,而半格高度有限,必然会逐渐收敛。可以证明,收敛到不动点,且它一定是最大的不动点。

(二)数据流分析基础

widening and narrowing

它的提出是为了解决数据流分析的复杂性,太过复杂会导致收敛速度极慢。

区间分析

以区间分析为例:

(二)数据流分析基础可以想到的是,如果正向进行,变量的范围应当是逐渐扩大的,即交汇操作满足

[a,b]⊓[c,d]=[min(a,c),max(b,d)]

变换函数表示这条语句自身导致变量的变化,例如加上一个变量或者变量组合。 

 

[a,b]+[c,d]=[a+c,b+d][a,b]−[c,d]=[a−d,b−c]

 

但是这样构成的半格高度是无限的,而且操作也不能保证单调性,因此提出了改进策略——人为指定上下界。如果下界大于类型的最大值,那么为空值,程序异常;如果下界小于最大值,那么更新下界和上界,其中如果最大值之和和类型最大值取其中小者。

 

{[a,b]+[c,d]=∅a+c>int−max(a+c,min(b+d,int_max))a+c≤int_max

 

基础 widening

但是这样做的复杂度还是很高,于是可以通过降低结果的精度来加快收敛速度。基本的 widening 的方法是降低格的高度,它的核心是把结果进一步抽象,通过单调函数 w 把原来的半格映射成新的格,也即f←w∘f。例如在区间分析中可以预定范围,

  • 定义有限集合:B={−∞,10,20,50,100,+∞}
  • 定义映射函数 ww([l,h])=[max{i∈B∣i≤l},min{i∈B∣h≤i}]

这样就可以把区间 [15, 75]、[11, 89]等等映射成 [10,100],也即 ?([15,75])=[10,100]。由于状态数大幅减少,所以很大程度上加快了收敛速度。

再比如,对于如下代码我们比较是否应用基础 widening 的区别:

1
2
3
4
5
6
y=0;
while(input){
    x = 7;
    x = x+1;
    y = y+1;
}

补充:需要理解什么是交汇的节点,比如循环的入口就是,可以理解为执行路径的交点。

有限集合为: ,0,1,7,+,每次循环第二行处的状态如下图所示:

(二)数据流分析基础

基础 widening 的安全性和收敛性

安全性需要保证:w(x)⊑x 这是容易确定的,因为原来的 f(x) 是单调的,那么构造合适的 w 即可。

收敛性由单调性容易得到保证。

一般的 widening

基础的 widening 的精度不高,而且精度和收敛速度是不能两全的,但是一般的 widening 方法可以在一定程度上提高性能。一般的 widening 同时参考更新前和更新后的值来猜测最终会收敛的值。设 widening 算子 $$,它是我们自定义的规则。那么推断节点新的值可以表示为:

 

 DATA v← DATA v∇fv(MEETv)

 

再次以之前的代码为例,但是我们更改规则

1
2
3
4
5
6
y=0;
while(input){
    x = 7;
    x = x+1;
    y = y+1;
}

节点交汇操作规则如下,其中 T 表示格的最高层的元素

(二)数据流分析基础可以对比分析以上提到的不同的方式:

(二)数据流分析基础

一般 widening 的安全性和收敛性

为了保证安全性,构造 widening 算子的时候需要注意:

 

(x∇y⊑x)∧(x∇y⊑y)

 

但是为了保证收敛性比较麻烦,没有通用的判断方法,因为 widening 算子与变换函数的趋势有关,也无法保证在半格上的单调性。

这里提及一种不收敛的情况,当多条路径交汇的时候,如果定义的交汇操作时逐个进行的,那么可能由于处理前驱节点的顺序不一样,造成不一样的结果。

narrowing

widening 是只产生的区间比实际的区间更加大,而 narrowing 会将区间变小。通过再次应用原始转换函数对 Widening 的结果进行修正,narrowing 的方法可以提高 widening 的精度。简单的说,就是在某一步就不采用 widening 的方法,而是用原始的函数。例如下图 x 的值的区间在第 5 步突然缩小了。

(二)数据流分析基础引入 narrowing 算子 Δ

 

DATAv←DATAvΔfv(MEETv)

 

例如算子定义如下,当区间出现无穷时,可以缩小区间。

(二)数据流分析基础

narrowing 的安全性和收敛性

这里核心是需要证明在 widening 基础上再使用 narrowing,也是安全的,保证不会出错。根据前面的定义,初始输入 I 经过任意路径上的多个状态转换函数后得到的值的交集(按照半格顺序取小),会大于交汇操作得到的值。而经过 widening 映射后的新的半格也会满足单调性,并且每个节点的值必须小于初始的的值。按照下图,可以知道即使是从 widening 后的不动点 IG 再使用原来的转换函数若干次,得到的值会比 widening 的更小(精确)。

(二)数据流分析基础

简单地说,如果算子满足如下条件就是安全的:

 

xΔy⊑y

 

narrowing 是不保证收敛的,即使收敛也不能保证能够快速收敛。

根据上图可以知道,使用 narrowing 后的结果是在两个不动点之间,但是无法判断是否收敛

原文始发于learner L:(二)数据流分析基础

版权声明:admin 发表于 2022年12月8日 上午8:05。
转载请注明:(二)数据流分析基础 | CTF导航

相关文章

暂无评论

您必须登录才能参与评论!
立即登录
暂无评论...