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)用于保证参数传入了一个污点数据。

数据流分析

设V为节点，D表示集合中元素

  • data(V,D) <- gen(V,D)
  • data(V,D) <- edge(V’, V), date(V’, D), !kill(V, D) # 注意一定要防止矛盾
  • data(entry,d)

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.