• 软件程序分析原理
• datalog编程

int count=0;Iterator<Student> iter = sudents.iterator();
while(iter.hasNext()){    Student s = iter.next();    if(s.getAge() < 18){        count++;    }}

int count = sudents.stream().filter(s -> s.getAge() < 18).count();

只需要用一行lambda表达式声明即可，程序自己会将sudents转为stream流，并通过filter定义的筛选内容计算最后的count值。

声明式就是如此，相对来说代码简洁、可读性也更强。这种编程语言就是一种DSL(领域特定语言，Domain Specific Language)，用于某一个特定领域的程序设计语言。而Datalog就是这样一种DSL，是Prolog的子集，其Datalog本名可以看作“Data+Logic”，接下来着重讲讲Datalog的一些理念。

Data

Data中包含了谓词和原子两个概念

谓词(Predicate)

如上这个表为balance表，则balance就是一个谓词，在balance表中("zhangsan",1800)表示“张三有1800元”，这是一个事实，而("lisi",5200)表示“李四有5200元”，该数据不存在，因此这不是一个事实。

原子(Atoms)

Logic

通常可以将Datalog的谓词分为两大类，即EDB和IDB：

• EDB（Extensional database）：EDB谓词是预先定义好的，通常不可变，作为datalog的输入（即外部传入，extensional）。

• IDB（Intensional database）：IDB 谓词通常由rules推导出，通常是datalog的输出。

并且在Datalog的规则中可以支持递归性

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

Datalog执行图介绍

Datalog的指针分析原理

我会在这一小节着重介绍Datalog是如何做指针分析，并重点从上下文不敏感分析和上下文敏感分析两个部分讲解。

上下文不敏感分析

在做上下文不敏感指针分析的时候，之前介绍的几个概念在这里分别代表如下角色：

• EDB：程序句法上可获得的指针相关信息。

• IDB：指针分析的结果。

• Rules：指针分析的规则。

EDB定义了变量集合为V，域为F，对象为O。并经过如New/Assign/Store/Load语句的时候，会提取如上语句为EDB：

• 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 ∈ 𝑝𝑡(𝑥)。pt是point-to set缩写。

• FieldPointsTo(oi : O, f: V, oj : O) ，如FieldsPointsTo(𝑜i, 𝑓, 𝑜j)表示𝑜j ∈ 𝑝𝑡(𝑜i.𝑓)。

最后综合EDB、IDB和Rules可以得出：

这里的Rule分母是IDB，分子是EDB。

读者如果在这里看不懂规则，可以停下来稍微多看几眼有个印象，并结合后续分析慢慢深入理解。

这里借用南大软件分析课程Reference[2]的图来讲解。

程序会先将EDB指令，变成如下表格形式

b = new C();c = new C();

之前介绍指针分析的IDB的时候说过VarPointsTo(x,oi)表示oi ∈ 𝑝𝑡(𝑥)。因此可以得出上图中的o1属于point(b)、o3属于point(c)。

再往后执行Rules，会解析Assign语句，看到之前的表格中的Statement中表达式是x = y，因此Example中属于x = y的表达式语句有如下：

a = b;d = c;

c.f = d;

在Example中Load语句对应的代码是e = d.f;。读者在这里可以看到，虽然Example中并没有直接对d.f字段的赋值操作，但是有对应的fact可以通过VarPointsTo查询到，并把oi带入FieldPointsTo对应上该f字段对应的o1和o3。如果读者在这里疑惑，为什么我Example中第4行c.f = a;赋值了a，并在第6行又覆盖了c.f字段的变量，而这里最后IDB中VarPointsTo中的值还是加上了a变量的o1？其实这就是上下文不敏感分析的原理，不会过度关注代码的执行逻辑，因此也有该分析的痛点：大大降低了分析的精度。

上下文敏感分析

这一章节会多引进几个EDB和IDB概念，在Call指令中的EDB，定义了S代表指令，M代表方法。且共有3条Rules：

先来看第一个Rule

引进了如下3个EDB和2个IDB：

• VCall(l:S,x:V,k:M)：调用本身的信息，指令l，变量x，方法k。

• Dispatch(o:O,k:M,m:M)：根据对象o给定的方法k，找到实际调用的方法m。

• ThisVar(m:M,this:V)：获取m方法中的this变量。

• Reachable(m:M)：表示m方法可达。

• CallGraph(l:S,m:M)：表示l指令到m方法有一条调用边。

如此一来就添加了方法调用的调用图。

再来看看第二个Rule中，该Rule是对参数传递的规则：

其中EDB的内容Arg和Param对应实参和形参

• Argument(l:S,i:N,ai:V)：对应方法调用中的实参，l是调用点，i是代表方法调用中的第几个参数（索引），a是对应的参数变量。

• Parameter(m:M,i:N,pi:V)：m是调用的函数，i是调用的参数索引，p对应的参数变量。

再来看看这个规则，如果存在l到m的CallGraph调用边，就取出实参ai和形参pi，并最终都指向o。

再来看看第三条Rule：

该Rule有两个EDB：

• MethodReturn(m:M,ret:V)：m被调用函数的返回值是ret。

• CallReturn(l:S,r:V)：l调用点所接收的变量是r。

规则会先判断l到m是否存在一条调用边，并取出m函数的返回值ret，以及查询ret指向的对象o，并和l调用点的接受变量r对应上。

全程序指针分析

Datalog污点分析原理

• EDB谓词：
• Source(m:M)：产生污点源的函数，通常是用户可控数据的输入点。
• Sink(m:M)：污点的汇聚点，污点在此处沉淀，并产出对应的分析报告。
• Taint(l:S,t:T)：关联调用点l和它产生的污点数据t的相关CallSite信息
• IDB谓词：
• TaintFlow(t:T,m:M)：表示污点数据t最终会在Sink函数m中汇聚。

小结

Datalog总体来说分析实现简单，只需要通过规则的编写和相关污点函数的定义就能对程序进行跟踪。这种涉及理念是不是觉得有点像LGTM的QL查询，只需要通过简单的声明式语言编写分析语句即可。对很多安全人员来说实现简单，可读性很强。同时上述指针分析和污点分析的形同点在于污点分析是关注Source到Sink的传播流，而指针分析是关注对象和变量之间的传播。

想去研究代码实践的读者们可以了解一下Reference[4]的jatalog项目，同时如果对这门分析课程感兴趣的读者也可以看看南大的李樾、谭添老师开的软件分析公开课（Reference[2]），相关详细的ppt也可以在（Reference[5]）中找到。

上章节介绍了Datalog的原理，以及如何进行数据流分析的。

Souffle是一款受Datalog启发的逻辑编程语言，其设计之初就是为了方便Oracle实验室的成员进行逻辑静态代码分析。Souffle支持的应用广泛，包括但不限于有Java的静态代码分析、并行编译器、二进制反汇编器、云计算的安全分析和智能合约的分析。而应用广泛且强大的Java指针分析程序Doop(Reference[1])就是以Souffle为datalog引擎。

这里我们就重点关注Souffle在ByteCodeDL中的实际应用部分。

先来学习一下Souffle的声明式表达是如何分析的

Souffle datalog声明式语言

Souffle中的主要语言元素是关系声明（relation declarations）、事实（facts）、规则（rules）和指令（directives）。

认识了上面我介绍的Datalog语法，再来看看Souffle是如何定义规则的。这里我在我的Ubuntu上装好了souffle引擎。假设有如下example.dl规则：

.decl edge(x:number, y:number).input edge
.decl path(x:number, y:number).output path
path(x, y) :- edge(x, y).path(x, y) :- path(x, z), edge(z, y).

.decl声明了一个edge关系，寓意x到y的一条有向边；path是声明了一个可达路径，表示x到y有一条可达路径。

.input <filename>会在当前目录中读取filename.facts文件内容。

而.output <filename>会输出一个filename.csv文件。

规则的最后两行表示：

1. 如果存在一条x到y的有向边(edge)，则表示也存在一条x到y的可达路径(path)。

2. 如果x到z有一条可达路径，且z到y存在一条有向边，则表示x到y也存在一条可达路径。

而input指定的edge.facts文件里面的内容是

1  22  3

之后在Ubuntu系统中通过以下命令运行souffle引擎检测：

$ ./souffle -F. -D. example.dl

参数设定：

• -F 指定了facts所在的目录

• -D 指定了输出目录

• example.dl 指定datalog文件名

之后output输出的path.csv结果集内容是

1  22  31  3

上述定义的变量是number数值类型，关于souffle支持的类型可以去souffle的官网查看，其类型大致分为如下四种：

• Symbol type: symbol

• Signed number type: number

• Unsigned number type: unsigned

• Float number type: float

Doop分析流程

1. 使用soot生成对应的jimple的IR文件。
2. 将jimple文件再转换datalog的facts。
3. 使用souffle引擎加载Rules并进行分析，并输出分析结果。

从Doot的分析流程中可以得出来，分析程序会分为上述三个步骤，我们再回过头来看看ByteCodeDL的分析。

通过Doot提供的一个Soot生成facts小工具，来生成对应的jar包中的facts。

java -jar soot-fact-generator.jar -i SIDemo.jar  -l /usr/lib/jvm/java-8-openjdk-amd64/jre/lib/rt.jar --generate-jimple --allow-phantom --full -d out

• -i 指定待分析的jar包
• -l 指定依赖库
• --generate-jimple 表示生成中间语言jimple
• --allow-phantom 大概是允许解析依赖不存在的类
• --full 表示对所有class进行解析
• -d 指定输出目录

进入out目录下面，会生成很多facts文件

但是我在这里发现一个bug，工具生成jimple并不支持SpringBoot程序。而需要soot生成对应的jimple文件是需要对应依赖项的，也就是需要把SpringBoot的lib下面的所有jar包加入到soot的classpath目录中。

于是乎我修改了Doop工具的soot-fact-generator生成工具，将判断-i参数指定的jar文件中是否存在“BOOT-INF/lib(classes)”的路径，如果存在则将路径下的所有依赖解压到当前目录的lib(classes)目录下，否则不做处理。

在生成过程中，如果遇到了OutOfMemory异常，并提示Java  heap space，则是给的堆空间小了，加上jvm参数-Xms200m -Xmx4096m即可(根据机器配置而定)。

如果你是跑在虚拟机上，一定要多给虚拟机几核CPU。因为程序中会通过循环遍历所有依赖的类，并生成对应的中间语言，我这里用的SpringBoot的靶场，Xmx参数可以给高一点，这样程序能更快的得出结果。之后就能在out/jimple目录下看到生成的中间语言。

至此，分析流程的三部曲已经完成前两步了，还差最后一步对生成的事实进行分析。

比如我这里想检索所有的方法中，有没有类名包含XSSController的方法，并输出。

于是我编写了如下的datalog规则：

#include "inputDeclaration.dl"
.decl QueryResult(class:Class, method:Method).output QueryResult
QueryResult(class, method) :-     MethodInfo(method, simplename, param, class, _, _, arity),    contains("XSSController", class),    arity = 1.

EDB中是从soot-fact-generator.jar工具生成的facts文件读入，并输出最后的csv结果。

至于inputDeclaration.dl，是针对souffle规则和生成好的facts定义的类和方法等属性名称。

打开inputDeclaration.dl文件，前几行就是基础变量属性定义

// 指令 可以定位出动作（比如call,load,sotre,assign）发生时的代码位置.type Insn <: symbol// 变量 .type Var <: symbol// 堆 也可以理解为内存中的对象.type Heap <: symbol// 字段.type Field <: symbol// 方法.type Method <: symbol// 类.type Class <: symbol

在里面就定义了上面用到的MethodInfo的EDB输入

可以明确看到

.input MethodInfo(IO="file", filename="Method.facts", delimiter="\t")

程序是直接从Method.facts中读入数据，并对其进行分析。

定义污点分析规则

先来看看污点源参数是如何定义的，这里拿之前的SpringBoot的靶场SIDemo来说明案例。

先来看看对应的XSSController的Jimple中间代码：

public java.lang.String reflection(java.lang.String){  org.sec.sidemo.web.XSSController this#_0;  java.lang.String message#_0, $stack3;  org.sec.sidemo.service.XSSService $stack2;
  this#_0 := @this: org.sec.sidemo.web.XSSController;
  message#_0 := @parameter0: java.lang.String;
  $stack2 = this#_0.<org.sec.sidemo.web.XSSController: org.sec.sidemo.service.XSSService xssService>;
  $stack3 = interfaceinvoke $stack2.<org.sec.sidemo.service.XSSService: java.lang.String reflection(java.lang.String)>(message#_0);
  return $stack3;}

这里我贴了XSSController的reflection方法的IR代码，其源代码如下图所示

可以很清楚的知道污点参数是reflection方法的第一个RequestParam注解的参数message，后经过xssService的reflection方法返回之后直接由@ResponseBody注解返回到了页面上。所以我们的首要目的就是讲该RequestParam注解的参数标记上污点。

这里我先贴出相关的souffle规则代码：

#include "inputDeclaration.dl"#include "utils.dl"#include "ptaint.dl"
.init ptaint = PTaint    //定义P/Taint指针分析
ptaint.cipt.Reachable("<org.sec.sidemo.web.XSSController: java.lang.String reflection(java.lang.String)>").    //定义入口函数
ptaint.SourceMethodArg("<org.sec.sidemo.web.XSSController: java.lang.String reflection(java.lang.String)>",0).  //因为后续会检测RequestParam注解是打在哪个参数上，所以这里的0不是this对象，而是reflection的参数。
.decl TaintVar(heap:Heap,var:Var)
TaintVar(heap,var) :-  ptaint.cipt.VarPointsTo(heap, var),    //heap就是污点标记，这里将污点标记到var上    ptaint.TaintHeap(_, heap).    //创建污点    //因为这两个EDB是逗号链接，所有heap必须满足两个条件，或者说两个EDB的heap变量必须相等
.output TaintVar

首先规则中定义了入口函数、Source点。在TaintVar查询语句中，有两个EDB，这两个EDB是经过ptaint中的IDB检索过来的，所以我们跟进PTaint规则中。

因为原先的规则并没有针对SpringBoot的，所以我这里添加了一条针对SpringBoot的参数定义污点的规则：

TaintHeap(insn, heap),    cipt.VarPointsTo(heap, to) :-        SourceMethodArg(callee,n),        AnnotationParam(callee,n,"org.springframework.web.bind.annotation.RequestParam"),        FormalParam(n, callee, from),        AssignLocal(_, _, from, to, callee),        ActualParam(_,insn,to),        heap = cat("NewArgTainted::", insn).

规则中首先查询了SouceMethodArg的callee方法，也就是我们刚才定义的

ptaint.SourceMethodArg("<org.sec.sidemo.web.XSSController: java.lang.String reflection(java.lang.String)>",0).

然后依据该callee到AnnotationParam中进行查询，查询该callee的索引为n的参数是否满足有RequestParam注解。

因为所有的参数注解都会在Param-Annotation.facts中呈现，所以我在inputDeclaration.dl规则中我添加了如下规则：

.decl AnnotationParam(method:Method, n:number, descriptor:symbol).input AnnotationParam(filename="Param-Annotation.facts")

再查询定义好的SourceMethodArg中的值

可以查询到对应的值，表示该Rule成立，继续往后看。后续带入到了FormalParam中查询对应的from值

正好对应了前面的jimple中间语言reflection的第一个参数parameter0，之后又使用了AssignLocal查询该parameter0转到了本地变量的哪一个值上。

查询的结果是<org.sec.sidemo.web.XSSController: java.lang.String reflection(java.lang.String)>/message#_0，正好对应jimple的parameter0转移。

之后通过ActualParam找到它对应的Insn的值，并用cat函数链接两个字符串传递给heap，从而得出最终的IDB。

读取最后生成的TaintVar结果集

就可以看到insn和var的值都输出到结果中，成功把污点标记到message#_0本地变量上。

既然污点源已经分析出来了，后续就要分析污点是如何传播的，且该Xss的Sink点的返回值是否包含污点标记(因为是ResponseBody注解修饰的方法，因此需要判断返回值是否有污点标记)。

污点是message参数，同时Controller中经过this.xssService.reflection(message)方法传递了污点，并把污点传递到了返回值上。

ptaint.ArgToRetTransfer("<org.sec.sidemo.service.XSSService: java.lang.String reflection(java.lang.String)>", 0).
.decl TransferTaint(heap:Heap, var:Var)
TransferTaint(heap, var) :-   ptaint.ArgToRetTransfer(callee, n),  VirtualMethodInvocation(insn, _, callee, _, _),  ActualParam(n, insn, arg),  ptaint.cipt.VarPointsTo(heap, arg),      //判断调用XSSService的实参是否是污点标记的对象  AssignReturnValue(insn, var).

如上，首先定义一个参数到返回值的转移规则，之后在TransferTaint的EDB里面判断了对应的方法调用，并判断对应的实参是否有污点标记。如果有，则用AssignReturnValue找到对应的返回值由什么参数接受，并输出IDB关联起heap和新的接受值var。

关联起来之后，只需要判断对应的Sink点的返回值是否和heap污点指向的参数值var相等即可判断是否存在XSS漏洞

ptaint.SinkMethod("<org.sec.sidemo.web.XSSController: java.lang.String reflection(java.lang.String)>", 0).
IsSink(TaintFlow) :-  TransferTaint(heap,var),  ptaint.SinkMethod(method,_),  Return(_, _, var, method),    //判断是否是Sink点的返回  TaintFlow = cat("TaintFlow:",cat(method,cat(">>>>>",heap))).

最终输出TaintFlow结果。

类型继承关系分析(CHA)原理刨析

在Java中相关的调用图分析有大致四种分析技术：

• Class hierarchy analysis(CHA)

• Rapid type analysis(RTA)

• Variable type analysis(VTA)

• Pointer analysis(k-CFA)

而其中Class Hierarchy Analysis(CHA)就是类型继承关系分析，其目的就是通过类之间的调用关系来分析程序的走向，相比较指针分析的方式，CHA的精度更低，但耗时更短。而且后续还需要投入大量的人力成本去排除可能存在的误报情况。本章节就简单的介绍CHA的分析原理和BytecodeDL是如何对靶场进行分析定位的。

在Java中，其方法调用可以分为四种调用：

• invokestatic

• invokespecial

• invokeinterface

• invokevirtual

invokestatic和invokespecial在编译解析的时候就能确定对应的调用方法是什么，而invokeinterface和invokevirtual无法在编译解析的时候无法知道是调用的何种方法，因此就需要

就好比重写方法的时候

Reachable(callee, n+1),CallGraph(insn, caller, callee) :-    Reachable(caller, n),    n < MAXSTEP,    VirtualMethodInvocation(insn, _, method, receiver, caller),    MethodInfo(method, simplename, _, _, _, descriptor, _),    VarType(receiver, class),    SubEqClass(subeqclass, class),    !ClassModifier("abstract", subeqclass),    Dispatch(simplename, descriptor, subeqclass, callee).

#define MAXSTEP 5#define CHAO 2
#include "inputDeclaration.dl"#include "utils.dl"#include "cha.dl"
SinkDesc("getInputStream", "java.net.HttpURLConnection").

EntryMethod(method),Reachable(method, 0) :-     MethodInfo(method, simplename, _, class, _, _, arity),    MethodModifier("public", method),    simplename = "ssrf1",  class = "org.sec.sidemo.web.SSRFController",    descriptor = "(Ljava/lang/String;)Ljava/lang/String;".
.output SinkMethod

neo4j-admin import --relationships=Call=/bytecodedl/neo4j/CallEdgeHeader.csv,/bytecodedl/output/CallEdge.csv --nodes=/bytecodedl/neo4j/CallNodeHeader.csv,/bytecodedl/output/CallNode.csv --nodes=/bytecodedl/neo4j/SinkMethodHeader.csv,/bytecodedl/output/SinkMethod.csv --database=$dbname --delimiter="\t" --skip-duplicate-nodes=true

MATCH n = (e:entry)-[*]->(s:sink) RETURN n

这一段时间的学习和接触发现白盒设计其实是非常聪明的，通过将程序转换成对应的facts，并用相关的datalog查询语句关联起对应的CallGraph和定义相应需要查询的规则数据库。之后通过neo4j类似的图形数据库来查询相应的漏洞。

对于ByteCodeDL来说，使用了Doop的Soot Facts生成工具，程序无法支持解析SpringBoot的程序，刚开始的时候和作者一样爬了不少的坑。看源码、改程序，但因为没有相关全面的文档，只能一点点通过自己的理解来更改相应的程序，但是觉得可以进一步发展以下功能：

• 更改Doop的Soot-Facts-Generate工具，增强对SpringBoot的支持。

• 因为目前ByteCode项目暂时只有对基础语法的支持，后续可以考虑增加定义Spring的Controller方法为入口函数，并增加相关漏洞Sink点的规则。

• 可以编写一个程序接口，专门添加入口函数和Sink的规则，后端再通过上传Jar包的功能自动化生成和导入图形数据库中。

• ByteCodeDL暂时只有作者提供的CHA查询规则，后续是否可以根据指针分析的规则添加相应的datalog查询。

其实ByteCodeDL和主流的CodeQL白盒工具原理相似，CodeQL有对数据流分析的支持，而ByteCodeDL处于刚开源的阶段，相关分析规则还不够完善。但好处在于ByteCodeDL提供了相关导入图形数据库查询的方式，方便安全人员甚至是开发人员查询相关漏洞，同时还有完整的图形显示，利于定位相关漏洞形成。

也很荣幸能够和作者认识，在学习ByteCodeDL的时候解答了我不少问题。

[1].https://bitbucket.org/yanniss/doop/

[2].https://www.bilibili.com/video/BV1wa411k7Uv

[3].https://anemone.top/pl-%E9%9D%99%E6%80%81%E7%A8%8B%E5%BA%8F%E5%88%86%E6%9E%90%E8%AF%BE%E7%A8%8B%E7%AC%94%E8%AE%B0%EF%BC%88Datalog%EF%BC%89/

[4].https://github.com/wernsey/jatalog

[5].https://pascal-group.bitbucket.io/lectures/Datalog.pdf

[6].https://yanniss.github.io/ptaint-oopsla17-prelim.pdf

[7].https://jckling.github.io/2021/12/17/Security/%E6%8C%87%E9%92%88%E5%88%86%E6%9E%90%E5%B7%A5%E5%85%B7%20Doop%20%E4%BD%BF%E7%94%A8%E6%8C%87%E5%8D%97/

[8].https://souffle-lang.github.io/docs.html

[9].https://www.cnblogs.com/xuesu/p/14321627.html

[10].https://blog.csdn.net/WDWAGAAFGAGDADSA/article/details/122906141

[11].https://www.jianshu.com/p/5cbc5bb5c4da