美文网首页软件源代码分析静态分析
【课程笔记】南大软件分析课程10——基于Datalog的程序分析

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

作者: bsauce | 来源:发表于2020-06-06 09:10 被阅读0次

目录:

  1. Motivation

  2. Datalog介绍

  3. Datalog实现指针分析

  4. 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节点和指针;如何处理相关语句中的变量。

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

原子AtomP(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:指针分析规则(与之前相同)。先分析上下文不敏感。

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

(2)上下文不敏感PTA示例

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

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

  1. 首先将EDB(指令)表示成表格数据形式。
  2. 处理New指令
  3. 处理Assign指令
  4. 处理Store指令
  5. 处理Load指令

(3)上下文敏感—全程序指针分析

call指令规则:S—指令,M—方法。共3条rule。

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

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

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

    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

规则:处理sourcesink函数。

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

课后问题:

  1. 有的调用图有多个main入口方法,咋办?

    将多个入口函数都加入到EntryMethod(m)即可。

  2. 有没有datalog和传统结合的做法

    如chord(java+Datalog实现)

相关文章

网友评论

    本文标题:【课程笔记】南大软件分析课程10——基于Datalog的程序分析

    本文链接:https://www.haomeiwen.com/subject/juxgzhtx.html