(七)抽象解释

(七)抽象解释

前言

这一文章是理论课,对之前的程序分析的合理性和思路,进行了理论上的分析和论证,有助于读者培养程序分析的思维。程序分析的很多思路都是对具体的值具体的表达式进行了抽象,建立了具体空间和抽象空间的关系,抽象解释理论就是解释映射函数。

(七)抽象解释

这个映射主要分成两部分:

  1. 具体化函数 γ 将抽象值映射为具体值的集合
  2. 抽象化函数 α 将具体值的集合映射为抽象值

伽罗瓦连接 Galois Connection

假设抽象域上存在偏序关系。简便起见,这里假设具体值集合上的偏序关系为子集关系。但抽象解释理论支持其他偏序关系,比如超集。

注意下面特殊的字 表示抽象域集合, 表示抽象域集合中的元素。任取两个集合中各自一个元素 X,那么如果满足如下的条件,就构成了伽罗瓦连接。

(七)抽象解释除了上面的定义意外,还有更加详细的定义,他们可以更加容易的看出映射函数的性质。为了加快学习速度,我不详细说明证明过程了。这让我想起来《信息安全数学基础》,学了一堆近世代数的东西,可能我当时不知道有什么特别的用途吧,但是认真学习下来确实锻炼了抽象化的能力,去考虑性质和映射。

(七)抽象解释

抽象域的安全性

我们探讨,抽象域上的操作,是否对于具体域是安全的,也就是说,不会包含预料外的结果。安全性 其实一个比较灵活的词,根据不同的分析会有不同的含义,比如指针分析是 may 分析,允许有超出实际指向的情况的结果,它的安全性就是包括了所有可能指向的对象。但是对于编译器优化来说,它为了保证语义,它的安全性是,一定不会改变语义才是安全的,也就是 must 分析。

可以证明,一定可以找到合适的变化的函数。

(七)抽象解释老师还以数据流分析的安全性为例,作了说明,后面还说明了路径的安全性。但是我暂时跳过了。感兴趣的读者可以见视频

常见抽象域

关系抽象

考虑变量之间的关系映射到抽象域上,这里以数值计算为例。老师举了一个比较巧妙地例子「八边形抽象」,用于理解关系抽象的约束,可以更加精确地分析。视频讲的很清楚不赘述了。

下面是一个区间分析,虽然我也不记得 narrowing 和 widening 的具体规则了,但是可以感受到,添加了 x+y x-y 这样的约束,可以更加精确地表示出 x y 的范围。

(七)抽象解释其他的数值抽象还有各种各样的图形,下面是比较简单的用平面图形就可以表示的情况,实际上高维的情况也是成立的,所以关系抽象是非常复杂但是应该也比较实用。

(七)抽象解释

谓词抽象

这个比较容易理解,把一堆属性,用谓词产生对应的真值序列或者矩阵。比如 x>0,x=0,x<0 就可以抽象成[true,false,false] 之类的。

体验抽象解释工具

最后,可以玩一玩这个抽象解释工具,这是一个用于教育意义的 demo。他自己设置了一个简单的语言,比如它给的例子

1
2
3
4
5
6
7
8
9
10
11
12
proc incr (x:int) returns (y:int)
begin
  y = x+1;
end

var i:int;
begin
  i = 0;
  while (i<=10) do
    i = incr(i);
  done;
end

矩形抽象域(box)下的结果,可以知道 incr 里面 x 的范围,接着就知道了 y 的范围,进而就知道了返回值 i 的范围。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
proc incr (x : int) returns (y : int) var ;
begin
  /* (L2 C5) [|x>=0; -x+10>=0|] */
  y = x + 1; /* (L3 C10)
                [|x>=0; -x+10>=0; y-1>=0; -y+11>=0|] */
end

var i : int;
begin
  /* (L7 C5) top */
  i = 0; /* (L8 C8) [|i>=0; -i+11>=0|] */
  while i <= 10 do
    /* (L9 C18) [|i>=0; -i+10>=0|] */
    i = incr(i); /* (L10 C16)
                    [|i-1>=0; -i+11>=0|] */
  done; /* (L11 C7) [|i-11=0|] */
end

八边形抽象域(octagon),可以得到 ±x+±y≥a 的形式的约束,具体生成过程就不细究了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
proc incr (x : int) returns (y : int) var ;
begin
  /* (L2 C5) [|x>=0; -x+10>=0|] */
  y = x + 1; /* (L3 C10)
                [|x>=0; -x+10>=0; -x+y-1>=0; x+y-1>=0; y-1>=0; -x-y+21>=0;
                  x-y+1>=0; -y+11>=0|] */
end

var i : int;
begin
  /* (L7 C5) top */
  i = 0; /* (L8 C8) [|i>=0; -i+11>=0|] */
  while i <= 10 do
    /* (L9 C18) [|i>=0; -i+10>=0|] */
    i = incr(i); /* (L10 C16)
                    [|i-1>=0; -i+11>=0|] */
  done; /* (L11 C7) [|i-11>=0; -i+11>=0|] */
end

 

原文始发于learner L:(七)抽象解释

版权声明:admin 发表于 2022年12月13日 上午8:00。
转载请注明:(七)抽象解释 | CTF导航

相关文章

暂无评论

暂无评论...