基于datalog构建自己的自动化静态代码审计分析工具(一)

简述
什么是 Datalog
- 概念介绍
  - 声明式语言
  - 自底向上
- 生态
  - Doop
  - 和 codeql 相比
实战
Continue

简述

曾梦想仗剑洞穿幽暗的代码，无物可挡扫描器的锋芒，天马行空的逻辑迷雾中框框出洞，了无隐患的牵挂，穿过无聊重复的业务逻辑，也曾因误报彷徨；当警报低鸣的瞬间，才见安全的世界清澈高远，盛开着永不凋零的自动化静态代码审计。

Datalog 是一种声明式逻辑编程语言。开源引擎，开源规则，使静态代码审计自动化充满无限可能

什么是 Datalog

维基百科说明

Datalog 是一种声明式逻辑编程语言。Datalog 通常采用自底向上的求值模型。它常被用作 演绎数据库（deductive databases）的查询语言 ，在数据集成、网络分析、程序分析等领域有广泛应用。

对其中一些关键点做些简单介绍

概念介绍

声明式语言

与声明式相对应的是命令式，声明式语言是一种编程范式

命令式语言语言举例

Set<Person> selectAdults(Set<Person> persons) {
  Set<Person> result = new HashSet<>();
    for (Person person : persons)
        if (person.getAge() >= 18)
            result.add(person);
    return result;
}

声明式语言举例

SELECT * FROM Persons WHERE Age >= 18;

codeql 就是声明式语言。

自底向上

从基础事实出发推导新结论

使用 https://github.com/BytecodeDL/ByteCodeDL/blob/main/docs/souffle.md 中的例子就是

// 声明 edge 表示 节点 x 到 y 有条边
// edge 具体数值已知，作为输入
.decl edge(x:number, y:number)

// 声明 path 表示 节点 x 到 y 有路径可达
// path 具体数值未知，作为输出
.decl path(x:number, y:number)

// 推理规则，如果x到y有边，那么x到y肯定有长度为1的路径，也就是如果x，y满足关系edge，也一定满足关系path
path(x, y) :- edge(x, y).

// 用到了递归推理，如果x到z有条路径，并且z到y有条边，那么就可以推理出x到y也有路径
path(x, y) :- path(x, z), edge(z, y).

如果给定输入值 edge

1 2
2 3

就能得到输出 path

2
3
3

生态

Datalog 是声明式语言

Souffle 是款 Datalog 推理引擎，也是著名声明式分析框架 Doop 默认的引擎。

Doop 使用 soot-facts-generator 生成事实推理库，也就是例子中的 edge 输入值

Doop

Doop 是一款静态代码分析框架，由雅典大学 PLaST 研究团队开发。

github 上 star 不太多，但是所有介绍都会称为 下一代静态代码分析框架。

和 codeql 相比

Doop 和 Codeql 同样都采取声明式语言进行代码分析。但是相较知名度而言不可同日而语

仅对技术部分进行说明：

维度	CodeQL	Doop
查询语言	自定义QL 声明式语言	标准Datalog 逻辑语言
引擎策略	闭源引擎（GitHub 维护优化）	开源（雅典大学科研团队开发）
语言支持	多语言：Java/Go/Python/C#/C++	仅限 JVM 生态（Java/Android）
分析输入	源码级（需编译分析AST）	解析.Class,分析jimple 文件
分析能力	污点追踪、控制流、语义漏洞扫描	高精度指针分析（上下文敏感）
集成部署	工业级 DevSecOps （GitHub CI/CD）	学术研究工具链（无原生 CI/CD 支持）
规则扩展	开源 6000+ 预置规则，支持自定义 QL	需编写 Datalog 规则

作为一个漏洞（bugbounty）挖掘者，能够获得源码包已经是跨过千难万险。相较而言 Doop 在这类场景下有独特优势。

实战

以最近的契约锁漏洞为例，简单介绍如何使用，便于理解 Datalog 声明式语言原理

找关注的方法

facts 元数据生成

主流是使用 soot 对class文件进行分析，然后生成facts 元数据。soot 是一款麦吉尔大学开发的java字节码分析工具

先使用soot解析 jvm class 文件生成 jimple 文件
再解析 jimple 输出逻辑元数据映射

生成数据结果如下

其中 jimple 文件夹是存放 class 文件解析后的中间文件
facts 是解析 jimple 中间文件生成的逻辑元数据

jimple 文件

以此次漏洞触发点重点关注对象为例，关注 setupcontroller#dbtest 方法。jimple 文件采用三地址码指令结构，消除jvm栈操作复杂性。

三地址码指令：可以被分解为一个四元组（4-tuple）：（运算符，操作数1，操作数2，结果）。因为每个指令最多包含三个变量，所以它被称为三地址码

三地址码结构比较清晰，不需要什么基础也能够读懂变量初始化，赋值，goto 跳转，函数调用等一系列逻辑

facts 元数据

以方法 Method.facts 中的一行数据为例，对method 方法进行声明

<com.qiyuesuo.setup.SetupController: com.qiyuesuo.common.AccessResult dbtest(com.qiyuesuo.core.config.DatabaseProperties)>  dbtest  com.qiyuesuo.core.config.DatabaseProperties com.qiyuesuo.setup.SetupController
com.qiyuesuo.common.AccessResult  (Lcom/qiyuesuo/core/config/DatabaseProperties;)Lcom/qiyuesuo/common/AccessResult; 1

method元数据每行包含4个字段，使用 \t分隔

methodId    simpleName    paramsSig    declType   retType    jvmSig    arity

各字段含义：

methodId: 方法的完整签名
simpleName: 方法名
paramsSig: 参数类型
declType: 声明该方法的类
retType: 返回值类型
jvmSig: JVM 格式的方法签名
arity: 参数个数

dl 查询语句构造

这样的话，如果我想找到类 SetupController 的 dbtest 方法

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

.decl MethodInfo2(method:Method, simplename:symbol, param:symbol, className:symbol, return:symbol, jvmDescriptor:symbol, arity:number)
.input MethodInfo2(IO=file, filename="Method.facts", delimiter="\t")

.decl QueryResult(className:symbol, method:Method)
.output QueryResult
QueryResult(className, method) :- 
    MethodInfo2(method, simplename, _, className, _, _, _),
    simplename = "dbtest",
    className = "com.qiyuesuo.setup.SetupController".

使用 souffle 引擎计算执行

souffle -F /mnt/hgfs/project4.3.7.bytecodedl4 -j auto -D /mnt/hgfs/ByteCodeDL/example/study/test_out/ test.dl

计算结果

root@toor:/mnt/hgfs/ByteCodeDL/example/study# cat test_out/QueryResult.csv
com.qiyuesuo.setup.SetupController      <com.qiyuesuo.setup.SetupController: com.qiyuesuo.common.AccessResult dbtest(com.qiyuesuo.core.config.DatabaseProperties)>

这个查询看起来意义不大，乏善可陈。那切换一个场景，找入口点。

注解

针对 spring 进行静态代码分析，其中一个重中之重就是处理spring语法糖 注解, 从spring 注解的使用，从 springmvc 路由，到自动装配，组件管理与依赖注入，外部化配置注入，数据库映射与访问抽象，但这些都是数据流的关键环。

springmvc 使用 org.springframework.web.servlet.mvc.method.annotation.RequestMappingHandlerMapping 做为框架注解类型，其他框架 jesery, MyFaces，apache cxf 框架也都使用各自的注解类型来减少开发量。

我们针对常见的 springmvc 框架编写

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


.decl MySourceMethod(method:Method)
.output MySourceMethod

MySourceMethod(method) :-
    (
     Method_Annotation(method, "org.springframework.web.bind.annotation.RequestMapping");
     Method_Annotation(method, "org.springframework.web.bind.annotation.GetMapping");
     Method_Annotation(method, "org.springframework.web.bind.annotation.PostMapping")
    ).

其中 Method-Annotation.facts 元数据中已经保存了方法和注解的关系，只需要匹配处理就可以

.decl Method_Annotation(method:Method, annotation:Annotation)
.input Method_Annotation(filename="Method-Annotation.facts")

语法说明

decl 定义了MySourceMethod 变量
output 用于输出到文件
括号用于分组，将内部的多个条件视为一个整体。
; 逻辑或 (OR)。表示括号内由分号分隔的多个条件中，只要有一个成立，整个括号内的表达式就为真。

输出入口方法如下

注解处理 challenge

需求

可以看到，这里对全量的入口方法进行了输出，我们想仅关注未授权逻辑

filter AccessControlFilter 使用 antpath 进行了路径是否需要授权判断，我们仅输出需要进行授权的方法路由

输出allowpath 如下

实现思路

路径拼接，方法中注解路径 + 类方法中注解
路径匹配，模拟实现 antpath ，进行授权路径匹配

难点注解元数据库修正

在使用 AnnotationElement.facts 元数据库时发现严重的数据缺失
小小注解大世界

type  com.qiyuesuo.setup.SetupController  0.0 0.0.0 - /setup  -

该文件每行包含 7 个字段，以制表符分隔：

AnnotationKind  AnnotatedElement  ParentId  ThisId**  Name  Value1  Value2

字段解释如下

AnnotationKind 表明这个注解是附加到哪种程序元素上的。有: type (类/接口), method, field, param。
AnnotatedElement 被注解的元素的唯一标识符。根据 AnnotationKind 的不同，其格式也不同。
- type: 类名 (e.g., com.example.MyClass)
- method: 方法签名
- field: 字段签名
- ParentId 父注解元素的 ID。
- ThisId 当前注解元素的 ID。
- Name 注解属性的名称。
- Value1 注解属性的值。
- Value2 额外的值。通常用于存储枚举类型的完整签名。

无值注解缺失

以SetupController 对象进行说明

@RestController
@RequestMapping(
    path = {"/setup"}
)
public class SetupController {
}

有两个注解 RestController 、 RequestMapping 但只输出一个 RequestMapping 值

属性传递缺失

/setup 路径的属性值时 RequestMapping 。路径拼接时需要多个 RequestMapping 注解值相加。但可以看到类样例中缺乏类型

注解复杂性太高

除了常见注解以外，java 注解支持嵌套。

但是在这里尝试使用一张二维表单去存储

第二个字段 AnnotatedElement 已经失去了类别概念。在读取时只能以字符串方式读取
嵌套定义，只能使用parentId， thisId 去进行关联。在单表读取时还涉及到递归赋值

实现复杂度高，二维表保存了太多结构语义。导致了数据缺失，出现了bug

修复

这里时facts 元数据生成问题，需要修改 doop 的 fact-generator 源码。

了解完原因

简单点从代码层面就只是缺啥补啥
彻底点是需要把AnnoationElements 表拆开

这里为了图思考简单选择方式1, 生成元数据库如下

类SetupController 有两个注解 RestController 和 RequestMapping ，序号值为 0.0 和 0.1

可以看到 RestController 的属性值 id 0.0.0 为空

RequestMapping 序号 0.1 , 属性值 0.1.0 ，属性值对为 path /setup

方法同理

自定义函数库

这里有两个步骤，

字符串拼接，类路径 + 方法路径
字符串匹配，路径和filter 指定路径匹配

这里使用了souffle 引擎自定义函数实现功能，支持 C/C++ 提供自定义函数

字符串拼接函数，按照 souffle 说明文档进行构造即可

root@toor:/mnt/hgfs/ByteCodeDL/example/study# cat /mnt/hgfs/ByteCodeDL/lib/concat.cpp
#include <souffle/SouffleInterface.h>
#include <string>

extern "C" {
souffle::RamDomain concat(
    souffle::SymbolTable* symbolTable,
    souffle::RecordTable*,
    souffle::RamDomain a,
    souffle::RamDomain b
) {
    const std::string& sa = symbolTable->decode(a);
    const std::string& sb = symbolTable->decode(b);
    std::string result = sa + sb;
    return symbolTable->encode(result);
}
}

dl 规则

最后使用dl 规则如下

root@toor:/mnt/hgfs/ByteCodeDL/example/study# cat ../source3.dl
#include "../logic/inputDeclaration.dl"

//导入自定义函数
.functor concat(a:symbol, b:symbol):symbol stateful
.functor pathMatch(path:symbol, pattern:symbol):number stateful

.decl AnnotationElement(kind:symbol, annotated:symbol, parent:symbol, this:symbol, name:symbol, value1:symbol, value2:symbol)
.input AnnotationElement(IO=file, filename="AnnotationElement.facts", delimiter="\t")

.decl ClassHeap(class:Class, className:symbol)
.input ClassHeap(IO=file, filename="ClassHeap.facts", delimiter="\t")

// 类上的注解类型
.decl ClassAnnotationType(class:Class, annotationType:symbol, rootId:symbol)
//.output ClassAnnotationType
ClassAnnotationType(class, annotationType, rootId) :-
    AnnotationElement("type", className, "0", rootId, annotationType, "-", "-"),
    ClassHeap(class, className),
    (
        annotationType = "org.springframework.web.bind.annotation.RequestMapping";
        annotationType = "org.springframework.web.bind.annotation.PostMapping";
        annotationType = "org.springframework.web.bind.annotation.GetMapping"
    ).

// 类上的 path 属性
.decl ClassPath(class:Class, path:symbol)
//.output ClassPath
ClassPath(class, path) :-
    ClassAnnotationType(class, annotationType, rootId),
    ClassHeap(class, className),
    AnnotationElement("type", className, rootId, _, "path", path, _).




// 方法上的注解类型
.decl MethodAnnotationType(method:Method, annotationType:symbol, rootId:symbol)
MethodAnnotationType(method, annotationType, rootId) :-
    AnnotationElement("method", methodSymbol, "0", rootId, annotationType, "-", "-"),
    MethodInfo2(method, _, _, _, _, _, _),
    method = methodSymbol,
    (
        annotationType = "org.springframework.web.bind.annotation.RequestMapping";
        annotationType = "org.springframework.web.bind.annotation.PostMapping";
        annotationType = "org.springframework.web.bind.annotation.GetMapping"
    ).

// 方法上的 path 属性
.decl MethodPath(method:Method, path:symbol)
//.output MethodPath
MethodPath(method, path) :-
    MethodAnnotationType(method, annotationType, rootId),
    AnnotationElement("method", method, rootId, _, "path", path, _).

.decl MethodInfo2(method:Method, simplename:symbol, param:symbol, className:symbol, return:Class, jvmDescriptor:symbol, arity:number)
.input MethodInfo2(filename="Method.facts")




.decl FullPath(method:Method, fullPath: symbol)
.output FullPath
FullPath(method, fullPath) :-
    MethodPath(method, methodPath),
    MethodInfo2(method, _, _, className, _, _, _),
    ClassHeap(class, className),
    ClassPath(class, classPath),
    fullPath = @concat("/api", @concat(classPath, methodPath)),
    (
        @pathMatch(fullPath, "/api/error*")=1;
        @pathMatch(fullPath, "/api/license/check")=1;
        @pathMatch(fullPath, "/api/license/get")=1;
  //这里省略其他的匹配操作...... 
    ).

最后输出效果如下

构造调用关系图

Doop 在学术界一直是标榜指针分析的效果。这里我们先简单些，做个基本的函数调用，完成简单版本的代码分析

调用关系

先来一个 dl 规则定义

CalleeMethod(insn, callee) :-
    GivenMethod(method),
    (
        SpecialMethodInvocation(insn, _, callee, _, method);
        StaticMethodInvocation(insn, _, callee, method);
        (
             VirtualMethodInvocation(insn, _, callee, base, method),
             MethodInfo(method, simplename, _, _, _, descriptor, _),
             VarType(base, class),
             Dispatch(simplename, descriptor, class, _)
        )
    ).

理论知识调用有三类

SpeicalMethodInvocation
StaticMethodInvocation
VirtualMethodInvocation 需要在运行时根据receiver实际类型才能确定被调函数。

以dbtest 方法为例

public AccessResult dbtest(DatabaseProperties dbProperties) {
        if (dbProperties.getDb() == null) {
            dbProperties.setDb(Database.MYSQL);
        }

        if (StringUtils.isBlank(dbProperties.getHost())) {
            return AccessResult.newFailureMessage("请填写主机名称!");
        } else if (dbProperties.getPort() < 1) {
            return AccessResult.newFailureMessage("请填写端口号!");
        } else if (StringUtils.isBlank(dbProperties.getName())) {
            return AccessResult.newFailureMessage("请填写数据库名称!");
        } else if (StringUtils.isBlank(dbProperties.getUsername())) {
            return AccessResult.newFailureMessage("请填写用户名!");
        } else {
            List<DbCheckResult> result = this.setupService.check(dbProperties);
            return AccessResult.newSuccessMessage(result);
        }
    }

方法调用

VirtualMethodInvocation

VirtualMethodInvocation 这是 Java 中最常见的方法调用类型。

这里使用 jimple 文件三地址码表达调用 Setupcontroller#dbtest 方法中调用

$stack3 = virtualinvoke dbProperties#_0.<com.qiyuesuo.core.config.DatabaseProperties: net.qiyuesuo.framework.db.Database getDb()>();

核心是代码

dbProperties.getDb()

实际上可以理解为

DatabaseProperties dbProperties = new DatabaseProperties ()
dbProperties.getDb()

StaticMethodInvocation

StaticMethodInvocation 静态方法调用

$stack5 = staticinvoke <net.qiyuesuo.common.lang.StringUtils: boolean isBlank(java.lang.CharSequence)>($stack4);

具体使用见下

StringUtils.isBlank()

SpecialMethodInvocation

特殊方法调用

指令: invokespecial

核心特点

非虚拟分派: 尽管它有 receiver（像虚拟调用一样作用于对象实例），但它不会进行动态分派。它会精确地调用在 callee 字段中指定的方法。
分析确定: 与静态调用类似，invokespecial 的目标在编译时也是确定的。调用图的边可以被精确地建立。

主要用途

构造函数调用 (<init>): 当你使用 new 关键字创建一个对象时，对该对象构造函数的调用就是通过 invokespecial 完成的。
私有方法调用 (private methods): 在一个类内部调用自己的私有方法。因为私有方法不能被子类覆盖，所以不需要动态分派。
super 调用: 在子类中调用父类的方法，如 super.someMethod()。这需要精确地调用父类的实现，而不是子类自己的（否则会无限递归）。

契约锁

最后效果，我们使用 controller 入口做为 source

使用危险函数做为sink

输出调用关系，这里可以使用 neo4j 做为观察图

一共输出三条路径， SetupController 的 dbtest / database 方法会调用 <java.sql.DriverManager: java.sql.Connection getConnection(java.lang.String,java.lang.String,java.lang.String)> 危险函数

<com.qiyuesuo.setup.SetupController: com.qiyuesuo.common.AccessResult dbtest(com.qiyuesuo.core.config.DatabaseProperties)>
<com.qiyuesuo.setup.SetupController: com.qiyuesuo.common.AccessResult database(com.qiyuesuo.core.config.DatabaseProperties)>

envInspect 方法会调用 Runtime

<com.qiyuesuo.setup.SetupController: com.qiyuesuo.common.AccessResult envInspect(java.lang.Long)>

这里是最后调用固定参数，误报

ProcessBuilder processBuilder = new ProcessBuilder(new String[]{"bash", "-c", "ulimit -u"});

如果未授权路径是有限的，人工代码审计甚至效率更快一点。

如果针对所有路径进行代码审计了。共计212 条记录，入口点一共有3586个，提效明显

212条记录中有很多相似路径，会重复命中关键函数关键调用，通过查询语句批量过滤无效逻辑，极大提高审计效率。

Continue

Datalog 的优势还是在指针分析，污点分析。如果要工程化，肯定是需要真正的污点分析而不是简单的函数调用
增加多场景匹配，dl 规则实现起来简单，引擎开源，可以针对 j2ee 场景做更多定制化的审计
1. thymeleaf 模板注入
2. mybaits 注入
3. 等等等等