【课程笔记】南大软件分析课程10——基于Datalog的程序分析（课时14）

重点：

Datalog语法，如何利用Datalog实现指针分析和污点分析。

本节课内容讲到了很多数据逻辑方面的应用，单上数理逻辑会觉得理论性太强，单上这节课的应用知识又觉得理论上不够严谨，总之算是一种互补。

1.Motivation

内容：了解命令式 vs 声明式语言，对比两种语言实现指针分析算法的优劣。

// 问题：从一群人中挑出成年人。
// 命令式语言(Imperative)：详细的命令机器怎么（How）去处理一件事情以达到你想要的结果（What）。如Java
Set<Person> selectAdults(Set<Person> persons) { 
  Set<Person> result = new HashSet<>();
  for (Person person : persons)
    if (person.getAge() >= 18)
      result.add(person);
    return result; 
}
// 声明式语言(Declarative)：只告诉你想要的结果（What），机器自己摸索过程（How）。如SQL，代码更简洁
SELECT * FROM Persons WHERE Age >= 18;

命令式语言—PTA：若采用命令式实现指针分析算法，实现复杂。需考虑worklist数据结构，是数组list还是链表，是先进先出还是先进后出；如何表示指针集合，hash集还是bit向量；如何关联PFG节点和指针；如何处理相关语句中的变量。

10-1-1-命令式语言.png

声明式语言—PTA：如何用声明式语言实现PTA？优点是简洁、可读性强、易于实现，例如Datalog。缺点是不方便表达复杂逻辑（Eg，for all全部满足）、不能控制性能。

2.Datalog介绍

Datalog（Data + Logic）：是声明式逻辑编程语言，可读性强，最初用于数据库。现在可用于程序分析、大数据、云计算。特点—没有副作用、没有控制流、没有函数、非图灵完备（精简了许多功能）。

（1）Data（谓词、原子）

谓词Predicate：看作一系列陈述的集合，陈述某事情是不是事实（真假）。如Age，表示一些人的年龄。

事实fact：特定值的组合。Eg，("Xiaoming", 18)。

10-2-1-谓词&fact.png

原子Atom：P(X1, X2, ... , Xn)。P表示谓词名，Xi表示参数（又叫term，可以是变量或常量）。Eg，Age("Xiaoming", 18) == true ；Age("Alan", 23) == false。

（2）Logic（Rule）

Rule：表示逻辑推导规则，若Body都为true，则Head为true。H <- B1, B2, ... ,Bn。H是Head，Bi是Body。 Eg，Adult(person) <- Age(person, age), age >= 18。

Rule要求：规则中的值要有限，如A(x) <- B(y), x > y；规则不能有悖论，如A(x) <- B(x), !A(x)。

Datalog中逻辑或：A或B都可推导出C，可写成C<-A. C<-B或者C<-A;B。

Datalog中逻辑非：!B(...)。

（3）Datalog谓词分类

EDB（extensional database）外延数据库：谓词需预先定义，关系不可变，可被当做输入。
IDB（intensional database）内涵数据库：谓词是根据规则建立的，关系是根据规则推导的，可被看作是是输出。

说明：H <- B1, B2, ... ,Bn，H只能是IDB，Bi可以是EDB或IDB。

递归性：Datalog支持递归，也即能够推导出自身。Eg，Reach(from, to) <- Edge(from, to)；Reach(from, to) <- Reach(from, node), Edge(node, to)。

（4）Datalog程序运行

Datalog程序运行：输入EDB+rules到Datalog引擎，输出IDB。常用Datalog引擎——LogicBlox, Soufflé, XSB, Datomic, Flora-2。

Datalog程序性质：单调性、终止性。

3.Datalog实现指针分析

（1）概念

EDB：程序句法上可获得的指针相关信息。如New / Assign / Store / Load语句。V-变量，F-域，O-对象。

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

IDB：指针分析结果。

VarPointsTo(v: V, o : O) ，如VarPointsTo(x,o_i)表示o_i ∈ 𝑝𝑡(𝑥)
FieldPointsTo(oi : O, f: V, oj : O) ，如FieldsPointsTo(𝑜_i, 𝑓, 𝑜_j)表示𝑜_j ∈ 𝑝𝑡(𝑜_i.𝑓)

Rules：指针分析规则（与之前相同）。先分析上下文不敏感。

10-3-1-上下文不敏感PTA规则.png

（2）上下文不敏感PTA示例

10-3-2-上下文不敏感PTA示例.png

步骤：其实指令处理顺序不固定。

首先将EDB（指令）表示成表格数据形式。
处理New指令
处理Assign指令
处理Store指令
处理Load指令

（3）上下文敏感—全程序指针分析

call指令规则：S—指令，M—方法。共3条rule。

首先找到调用的目标函数m，传递this指针。

10-3-3-call规则1.png
传递参数

10-3-4-call规则2.png
传返回值

10-3-5-call规则3.png

全程序指针分析：引入程序入口函数m。

10-3-6-全程序分析PTA-Datalog.png

4.Datalog实现污点分析

EDB谓词-输入：

Source(m : M) ——产生污点源的函数
Sink(m : M) ——sink函数
Taint(l : S, t : T) ——关联某callsite l和它产生的污点数据t

IDB谓词-输出：

TaintFlow(t : T, m : M) ——表示污点数据t会流向sink函数m

规则：处理source和sink函数。

10-4-污点分析规则.png

课后问题：

有的调用图有多个main入口方法，咋办？

将多个入口函数都加入到EntryMethod(m)即可。
有没有datalog和传统结合的做法

如chord（java+Datalog实现）