南大软分课程笔记｜14 基于Datalog的静态分析

前言

在之前的实验中，我们都是用Java编程实现相关的分析。包括Java在内，大多数编程语言都是命令式（imperative）的，我们通过编程来告诉计算机一步步需要做什么。除了命令式语言外，还有一类声明式（declarative）的语言，如SQL、Prolog和本节将要介绍的Datalog。我们可以简单认为Datalog语言是升级版SQL语言，同时在语法层面又是Prolog语言的子集。

下面两个代码片段实现了相同的功能，但分别采用了命令式语言和声明式语言。

首先是命令式：

Set<Person> selectAdults(Set<Person> persons) {
	Set<Person> result = new HashSet<>();
    for (Person person : persons)
        if (person.getAge() >= 18)
            result.add(person);
    return result;
}

接着是声明式：

SELECT * FROM Persons WHERE Age >= 18;

可以看出，声明式语言的代码更为简洁，忽略了很多实现相关、算法无关的细节。事实上，使用Datalog这种声明式语言来实现程序分析算法也要比使用命令式语言简单，最终产物也更简洁、可读。

Datalog简介

以下内容来自维基百科：

Datalog is a declarative logic programming language. While it is syntactically a subset of Prolog, Datalog generally uses a bottom-up rather than top-down evaluation model. This difference yields significantly different behavior and properties from Prolog. It is often used as a query language for deductive databases. Datalog has been applied to problems in data integration, networking, program analysis, and more.

Datalog，拆开就是Data+Logic，它有四个特点：无副作用，无控制流，无函数，非图灵完备。

Predicates (Data)

在Datalog中，predicate（谓词）是一个声明集合，可以类比为数据表。一个fact则是针对某个特定tuple是否属于一个关系的断言——针对给定的值的组合，某predicate为真。例如，假设有一个predicate（table）是Age，包含person和age两个column，那么("Xiaoming", 18)为真（fact），当且仅当这个元组存在于Age predicate中。

Atoms

Atoms是Datalog中的基本元素，用来以下面这种形式表示predicate：

P(X1, X2, ..., Xn)

其中P是predicate名，后面跟的X1～Xn是arguments（terms）。Terms可以是Variables（变量）或Constants（常量）。例如，Age("Xiaoming", 18)就是一个atom。P(X1, X2, ..., Xn)又称作relational atoms，当且仅当谓词P包含X1到Xn描述的元组时，它才为真。除了relational atoms外，Datalog还有arithmetic atoms，如age >= 18。

Datalog Rules (Logic)

规则是Datalog中表示逻辑推理的形式，用于说明facts的推导过程。Datalog中基本的规则形式如下：

H <- B1, B2, ..., Bn.

H表示head（consequent），是一个atom；B1～Bn表示body（antecedent），Bi也是atom（可以是否定的），每个Bi都是一个subgoal。上述规则的意思是：当body为真时，head为真。另外，其中的逗号,表示逻辑与，即，B1～Bn所有subgoals均为真时，body才为真，继而head才为真。例如，我们可以用如下规则推导出成年人：

Adult(person) <- Age(person, age), age >= 18

上述规则的解析过程如下：

• 考虑所有subgoals中的变量的值的所有可能组合。
• 如果某个组合能够让所有subgoals为真，则head atom也为真。
• head谓词包含所有true atoms。

在Datalog中有两种方式表示逻辑或：一种方式是用分号;连接，另一种方式是写多个head相同的规则。需要注意的是，Datalog中也有运算符优先级，“逻辑或”低于“逻辑与”，因此括号有时必不可少。

感叹号!则表示对某atom的否定，如!B(...)。

需要注意的是，下述规则是不安全的（因此也不被Datalog允许）：

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

为什么它们是不安全的？因为这两个规则都没有对x进行有效限制，意味着可以满足规则的x是无限的，这将导致A是一个无穷尽的关系。第二个规则可能具有一些迷惑性，但是它确实也是不安全的——也许C(x, y)对x进行了限制，但是对它取否定则导致x无限制。只有当规则内的每个变量至少出现在一个非否定的关系atom中时，这个规则才是安全的。

下面是一个规则解析的例子：

那么，初始数据，或者说那些facts，来自哪呢？

EDB和IDB谓词

Datalog中的谓词分为两部分：EDB（extensional database）和IDB（intensional database）。前者是预先定义的，作为程序输入，且不可变；后者是由规则创建的，关系由规则推理而来，可以看做程序的输出。

对于一条规则H <- B1, B2, ..., Bn.来说，H只能是IDB，Bi则可以是EDB或IDB。

递归

Datalog支持递归的规则，允许IDB谓词的自推导。例如，我们在计算图上的可达性信息（传递闭包）时，就需要递归规则：

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

正是递归赋予了Datalog超出SQL的强大能力。也因此，我们能将其用于复杂程序分析中。

另外注意，下面这样的规则是不可行的：

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

它是自相矛盾而无意义的。例如，在B(1)为真时，如果A(1)为真，则得出A(1)为假，反过来类似，都是矛盾的。因此，在Datalog中，对同一atom的递归和否定必须分开，否则该规则可能无法收敛。

Datalog程序的执行过程

Datalog引擎的输入是EDB和rules，输出是IDB。引擎将根据输入来推理facts，直到没有新facts产生。常见的引擎有LogicBlox、Soufflé、XSB、Datomic和Flora-2等。

我们在之前的学习中提到过单调性。事实上，Datalog是单调的，也就是说，已经产生的facts不会被删除。

我们说Datalog程序是可终止的，因为：Datalog是单调的，且在规则安全的前提下，IDB谓词的可能值是有限的。

基于Datalog的指针分析

下面，我们来研究一下如何基于Datalog实现（上下文不敏感的）指针分析。首先明确一下输入输出：

• 规则：指针分析规则，包括New、Assign、Store、Load（先不考虑Call规则）。

• EDB：从程序中提取的指针相关的信息，包括：

  • New(x:V, o:O)
  • Assign(x:V, y:V)
  • Store(x:V, f:F, y:V)
  • Load(y:V, x:V, f:F)

• IDB：指针分析结果，包括：

  • VarPointsTo(v : V, o : O)
  • FieldPointsTo(oi : O, f : F, oj : O)

我们结合一个案例来分析：

1 b = new C();
2 a = b;
3 c = new C();
4 c.f = a;
5 d = c;
6 c.f = d;
7 e = d.f;

EDB输入如下：

下面是之前我们总结的指针分析规则：

这些规则对应的Datalog规则如下：

VarPointsTo(x, o) <- New(x, o).
VarPointsTo(x, o) <- Assign(x, y), VarPointsTo(y, o).
FieldPointsTo(oi, f, oj) <- Store(x, f, y), VarPointsTo(x, oi), VarPointsTo(y, oj).
VarPointsTo(x, o) <- Load (y, x, f), VarPointsTo(x, oi), FieldPointsTo(oi, f, oj).

Datalog在实现上的确十分简洁。这里就不展示推理过程了，感兴趣的同学可以自行学习一下课件。

最后来看一下如何处理Call规则：

种类	语句	规则
Call	l: r = x.k(a1, ..., an)

Call规则比较复杂，其对应的新增EDB如下：

• VCall(l:S, x:V, k:M)
• Dispatch(o:O, k:M, m:M)
• ThisVar(m:M, this:V)
• Argument(l:S, i:N, ai:V)
• Parameter(m:M, i:N, pi:V)
• MethodReturn(m:M, ret:V)
• CallReturn(l:S, r:V)

新增的IDB如下：

• Reachable(m:M)
• CallGraph(l:S, m:M)

我们需要三条Datalog语句来表示Call规则：

VarPointsTo(this, o), Reachable(m), CallGraph(l, m) <- VCall(l, x, k), VarPointsTo(x, o), Dispatch(o, k, m), ThisVar(m, this).
VarPointsTo(pi, o) <- CallGraph(l, m), Argument(l, i , ai), Parameter(m, i, pi), VarPointsTo(ai, o).
VarPointsTo(r, o) <- CallGraph(l, m), MethodReturn(m, ret), VarPointsTo(ret, o), CallReturn(l, r).

最终，针对之前的代码段，我们得出如下Datalog分析规则：

Reachable(m) <- EntryMethod(m).
VarPointsTo(x, o) <- Reachable(m), New(x, o, m).
VarPointsTo(x, o) <- Assign(x, y), VarPointsTo(y, o).
FieldPointsTo(oi, f, oj) <- Store(x, f, y), VarPointsTo(x, oi), VarPointsTo(y, oj).
VarPointsTo(x, o) <- Load (y, x, f), VarPointsTo(x, oi), FieldPointsTo(oi, f, oj).
VarPointsTo(this, o), Reachable(m), CallGraph(l, m) <- VCall(l, x, k), VarPointsTo(x, o), Dispatch(o, k, m), ThisVar(m, this).
VarPointsTo(pi, o) <- CallGraph(l, m), Argument(l, i , ai), Parameter(m, i, pi), VarPointsTo(ai, o).
VarPointsTo(r, o) <- CallGraph(l, m), MethodReturn(m, ret), VarPointsTo(ret, o), CallReturn(l, r).

注意，我们在开头增加了规则，用于把entry加入到Reachable中，实现初始化。

基于Datalog的污点分析

在指针分析的基础上，我们来研究一下如何基于Datalog实现污点分析。

结合之前学习的污点分析流程，我们额外增加的EDB谓词如下：

• Source(m:M)
• Sink(m:M, i:N)
• Taint(l:S, t:T)

新增的IDB谓词如下：

• TaintFlow(sr:S, sn:S, i:N)

其中i:N表示sink call site的第i个参数。

下面是我们之前学习过的污点分析新增的规则：

种类	语句	规则
Call	l: r = x.k(a1, ..., an)
Call	l: r = x.k(a1, ..., an)

对此，我们新增两条Datalog规则：

VarPointsTo(r, t) <- CallGraph(l, m), Source(m), CallReturn(l, r), Taint(l, t).
TaintFlow(j, l, i) <- CallGraph(l, m), Sink(m, i), Argument(l, i, ai), VarPointsTo(ai, t), Taint(j, t).

总结与思考

本节课，我们初步学习了Datalog语言以及它在程序分析上的应用。

可以发现，Datalog的优点很明显：简洁、可读、易于实现。另外，Datalog引擎的性能将直接影响到程序分析效果。它的缺点同样明显：无法充分表达某些逻辑（例如，非全程单调的分析），另外其性能是无法充分控制的，受引擎限制。

以后要找机会实践一下！