目录:
Motivation
Datalog介绍
Datalog实现指针分析
Datalog实现污点分析
重点:
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节点和指针;如何处理相关语句中的变量。
声明式语言—PTA:如何用声明式语言实现PTA?优点是简洁、可读性强、易于实现,例如Datalog。缺点是不方便表达复杂逻辑(Eg,for all全部满足)、不能控制性能。
2.Datalog介绍
Datalog(Data + Logic):是声明式逻辑编程语言,可读性强,最初用于数据库。现在可用于程序分析、大数据、云计算。特点—没有副作用、没有控制流、没有函数、非图灵完备(精简了许多功能)。
(1)Data(谓词、原子)
谓词Predicate:看作一系列陈述的集合,陈述某事情是不是事实(真假)。如Age,表示一些人的年龄。
事实fact:特定值的组合。Eg,("Xiaoming", 18)。
原子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, Soufflé, 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,oi)表示oi ∈ 𝑝𝑡(𝑥)
- FieldPointsTo(oi : O, f: V, oj : O) ,如FieldsPointsTo(𝑜i, 𝑓, 𝑜j)表示𝑜j ∈ 𝑝𝑡(𝑜i.𝑓)
Rules:指针分析规则(与之前相同)。先分析上下文不敏感。
(2)上下文不敏感PTA示例
步骤:其实指令处理顺序不固定。
- 首先将EDB(指令)表示成表格数据形式。
- 处理
New
指令 - 处理
Assign
指令 - 处理
Store
指令 - 处理
Load
指令
(3)上下文敏感—全程序指针分析
call指令规则:S—指令,M—方法。共3条rule。
-
首先找到调用的目标函数m,传递this指针。
-
传递参数
-
传返回值
全程序指针分析:引入程序入口函数m。
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
函数。
课后问题:
-
有的调用图有多个main入口方法,咋办?
将多个入口函数都加入到EntryMethod(m)即可。
-
有没有datalog和传统结合的做法
如chord(java+Datalog实现)