0%

静态程序分析课程笔记(Datalog)

先前的分析算法虽然展示了分析细节,但是过于复杂难以实现,本课将介绍一种一种声明式语言(Datalog)以数据驱动推导的方式做指针分析和污点分析

Motivation

Imperative vs Declarative

Imperative(命令式)语言主要有Java、C/C++等,展示了详细的实现细节;

Declarative(声明式)语言主要有SQL等,其屏蔽细节,因此代码量更小,可读性更强。

如对于查找成年人的程序,命令式语言实现如下:

1
2
3
4
5
6
7
Set<Person> selectAdults(Set<Person> persons) {
Set<Person> result = new HashSet<>();
for (Person person : persons)
if (person.getAge() >= 18)
result.add(person);
return result;
}

而声明式语言实现如下:

1
SELECT * FROM Persons WHERE Age >= 18;

可见命令式语言主要强调如何做,而声明式语言强调的是做什么。

Introduction to Datalog

Datalog 是一种声明式语言,是 Prolog 的子集,最早用于数据库查询[1],而如今已经被用于程序分析、大数据、云计算等多个领域

Datalog 即 “Data+Logic”,其程序没有控制流,没有函数,不是一个图灵完备的语言。

Data

Predicates

Datalog 中数据用谓词(Predicates)表示,具体来说,谓词是一张数据表,表中的每条数据反应一个事实(fact)。

person age
xiaoming 18
xiaohong 23

如以上为Age表,Age就是一个谓词,而在Age中 ("xiaoming",18) 表示“小明是18岁“,这是一个事实,而("xiaohong",22)表示 “小红是22岁”,表中没有这个数据,因此这不是一个事实。

Atoms

Datalog中的谓词用 Atom 表示,一个 Atom (实际上是关系型原子——relational atom)形如P(X1,X2,...,Xn),其中 P 表示谓词名称,而X1,X2,...,Xn 表示谓词的参数(Arguments/terms),参数是可为变量或是常量,若表中存在数据,则关系型数据为真,否则

例如先前Age谓词,有如下Atoms:

  • Age(person, age)
  • Age("xiaoming", 18)

Atom 另一类称为算数型原子(arithmetic atoms),由算数表达式组成,例如:

  • age >= 18

Logic

Rules

Rules 在 Datalog 中定义了facts的推导过程,一个rules形如 H <- B1, B2, ... ,Bn,其中 H (head)为一个 atom,表示结论(consequent),B1,B2,...,Bn (body)表示前提条件(antecedent),Bi表示一个子目标(subgoal),, 表示逻辑与关系,即上例表示“当B1、B2、…、Bn都成立时,H成立”。

Datalog 运行时将不断从已知事实中推出新事实,当无法再推出新的事实时,程序停止。

EDB和IDB

通常来说,Datalog 有两类谓词,EDB和IDB:

EDB(Extensional database):EDB谓词是预先定义好的,通常不可变,作为datalog的输入(即外部传入,extensional)

IDB(Intensional database):IDB 谓词通常由rules推导出,通常是datalog的输出。

Logical Or

有两种方式表示逻辑或:

  1. 编写多条推导规则,如:

    1
    2
    GradeOne(Person) <- Age(person,17).
    GradeOne(Person) <- Age(person,17).
  2. ;分割条件,如:

    1
    GradeOne(person) <- Age(person,17);Age(person,18).

注意,; 优先级低于,,如优先做;需加()

Negation

! 表示取反,如:

1
Man(person)  <- Age(person, age), age>=18, !Gender(person,"woman").

Recursion

Datalog 支持递归推导,如计算图的可达性:

1
2
Reach(from,to) <- Edge(from, to).
Reach(from,to) <- Reach(from, node), Reach(node, to)

正是由于支持推导,才让Datalog足够强大,以至于能做复杂的程序分析。

Rule Safety

考虑如下两种写法:

  • A(x) <- B(y), x > y
  • A(x) <- B(y), !C(x,y)

由于y没有范围限制,因此规则推导过程时无限的。

Datalog中规则需要满足安全性(rule safety),即rule中每个变量至少出现在一个非反的 relation atom 中。

Recursion and Negation

考虑如下语句:

1
A(x) <- B(x), !A(x)

原子递归推导了自己的非,因此语句时矛盾的,即一个原子的递归和取反必须是分离的。

Excution

Datalog输入EDB和Rules,经过Data engine不断推导,最终产生IDB。

image-20200906204334359

Datalog程序一定会停止,因为:

  1. datalog是单调的——datalog的facts无法删除;
  2. datalog中IDB的谓词是有限的——考虑到rule safety。

常用的Datalog引擎有:

LogicBlox, Soufflé, XSB, Datomic, Flora-2, …

Pointer Analysis via Datalog

在Datalog中做指针分析时,EDB为语法上能直接获取的信息,IDB为指针分析的结果
,Rules为指针分析的规则。

Datalog Model

定义变量集合为 V,域为 F,对象为 O

那么EDB可以定义为:

Kind Statement EDB
New i: x = new T() New(x : V, o : O)
Assign x = y Assign(x : V, y : V)
Store x.f = y Store(x : V, f : F, y : V)
Load y = x.f Load(y : V, x : V, f : F)

定义IDB:

  • VarPointsTo(v: V, o: O)
    VarPointsTo(x, oi) 表示 $o_i \in pt(x)$
  • FieldPointsTo(oi: O, f: V, oj: O)
    FieldPointsTo(oi, f, oj) 表示 $o_j \in pt(o_i.f)$

Rules

将推导规则写为Datalog的规则:

Kind Statement Rule Datalog
New i: x = new T() $\frac{}{o_i \in pt(x)}$ VarPointsTo(x, o) <- New(x, o).
Assign x = y $\frac{o_{i} \in p t(y)}{o_{i} \in p t(x)}$ VarPointsTo(x, o) <- Assign(x, y), VarPointsTo(y, o).
Store x.f = y $\frac{o_i \in pt(x),\\ o_j \in pt(y)}{o_j \in pt(o_i.f)}$ FieldPointsTo(oi, f, oj) <- Store(x, f, y), VarPointsTo(x, oi), VarPointsTo(y, oj).
Load y = x.f $\frac{o_{i} \in pt(x),\\ o_{j} \in pt\left(o_{i} . f\right)}{o_{j} \in p t(y)}$ VarPointsTo(y, oj) <- Load(y, x, f), VarPointsTo(x, oi), FieldPointsTo(oi, f, oj).

下面举例说明

初始阶段,从程序中提取New,Store,Assign,Load语句为EDB:
image-20200906211135591

接下来处理New语句,将b、c加入VarPointsTo:
image-20200906211304812

处理Assign, 由$Assign(d,c), VarPointsTo(c, o_3) \rightarrow VarPointsTo(d,o_3)$ :
image-20200906211352710

处理Store,由

$Store(c,f,a), VarPointsTo(c,o_3), VarPointsTo(a, o_1) \rightarrow FieldsPointsTo(o_3,f, o_1)$,

$Store(c,f,d), VarPointsTo(c,o_3), VarPointsTo(d, o_3) \rightarrow FieldsPointsTo(o_3,f, o_3)$:

image-20200906211446132

处理Load,由

$Load(e,d,f), VarPointsTo(d,o_3), FieldPointsTo(o_3,f,o_1) \rightarrow VarPointsTo(e, o_1)$;

$Load(e,d,f), VarPointsTo(d,o_3), FieldPointsTo(o_3,f,o_3) \rightarrow VarPointsTo(e, o_3)$:

image-20200906211517749

注意在实际运行时,当新fact产生后,engine 会检查当前状态,处理能够推导的rules。

Handle Method Calls

处理函数调用需要添加新的EDB和IDB,并且定义三条规则:

  1. Dispatch,传this,建立一个call graph边
    image-20200906211906002

  2. 传参数,argument和parameter表示实参和形参
    image-20200906212005590

  3. 传返回值
    image-20200906212036419

做全程序指针分析时需要引入一个入口EDB,以下为完整代码
image-20200906212109286

注意,如果m不可达,那么它们的VarPointsTo永远为空,因此其他推导不需要加Reachable(m)

Taint Analysis via Datalog

在Datalog上做污点分析时,需要额外定义以下EDB和IDB

  • EDB

    • Source(m: M),定义函数 m 为source
    • Sink(m: M),定义函数 m 为sink
    • Taint(l: S, t: T), taint(l,t) 表示在l行产生了污点t,用于关联callsite产生的污点数据
  • IDB

    • TaintFlow(t: T, m: M),表示污点T流向M方法

在Call语句上新增如下推导:

  • 处理source:
    image-20200907211233439

    将返回值标记为污点。

  • 处理sink:
    image-20200907211324230

    n表示任意一个参数,Taint(_,t)用于保证参数传入了一个污点数据。

Conclusion

Datalog作为新兴的程序分析模型,有如下优点:

  1. 分析实现简单;
  2. 可读性强;
  3. 分析效率可以从高度优化Datalog引擎获益。

然而它的优点也正是它的缺点:

  1. 限制表达,没法表达特殊情况,如先前的gen-kill,以为datalog只能递增,又例如datalog很难表达所有条件都满足的情况(只能一个一个加);
  2. 效率严重依赖引擎,无法完全控制引擎性能。

个人感觉Datalog很像目前流行的LGTM思路,但是确实感觉表达不是很自由,然而它被很多大佬认为是未来主流的程序分析框架,还是值得学习的。

References

  1. David Maier, K. Tuncay Tekle, Michael Kifer, and David S. Warren, “Datalog: Concepts, History, and Outlook”. Chapter, 2018.