专栏名称: 利刃信安
利刃信安
目录
相关文章推荐
秋叶PPT  ·  哪吒这页PPT怎么做的?文字浮动太高级了! ·  10 小时前  
旁门左道PPT  ·  PPT重点别再标红了!!丑爆了! ·  23 小时前  
秋叶PPT  ·  夸爆!WPS官方接入DeepSeek,自动化 ... ·  昨天  
跟我学个P  ·  用DeepSeek为《哪吒2》做了份PPT, ... ·  3 天前  
秋叶PPT  ·  DeepSeek公务员上岗!雷军:真心建议普 ... ·  3 天前  
51好读  ›  专栏  ›  利刃信安

【代码审计】一种全新的代码审计技术:SyntaxFlow

利刃信安  · 公众号  ·  · 2024-06-14 17:48

正文

一种全新的代码审计技术:SyntaxFlow

代码审计技术在过去的一段时间的发展中,似乎受到了一个魔咒,安全从业人员的很难摆脱 *QL的影响,毕竟编译成数据库,然后通过 QL 来查询。或者通过把 AST 解析进 neo4j,通过 neo4j 的 QL: Cypher 或 API 来查询。甚至于我们在不使用 *QL 式的辅助工具的时候,也会通过 IDE 的 Query(关键字查询,定义查询,文件搜索)。甚至于我们也会戏称“搜索”是“代码审计”的核心操作。现状确实是这样,但是以搜索为切入点也会遇到其他的问题:



  • 如何搜索一个变量是函数调用?

  • IDE 提供了 Control/Command + 鼠标左键点击跳转的功能,代码审计工具一般很难提供这种功能。
  • 真实的漏洞往往跨越了很多个数据流,如何在不同数据流之间搜索?

以至于在大热门 CodeQL 的使用中,大部分操作均是在“对接数据流”和定义 Sink Source 等。



“代码分析”与“数理证明“


在学术圈的代码分析技术(算法)中,我们在这里指的是(在 SMT 或者 SAT 求解器理论中)我们需要把代码问题转化成符号运算与定理证明问题。然后通过约束求解算法找到“符号解(可能无法求解)”,如果有符号解的话,把符号解转化成具体的代码位置,找到 source 和 sink 的交汇点。

这一段话非常抽象,如果阅读这个抽象描述有问题的话,可以阅读以下 ChatGPT-4 的解读。
这段话概述了使用符号执行和约束求解技术(特别是在 SMT 或 SAT 求解器上下文中)来进行代码分析的基本过程。这里提供了对这一技术的高层次描述,并说明了其在识别代码中的安全漏洞(如 source 到 sink 的数据流问题)方面的应用。以下是对这一技术描述的几个关键点的评价:
正确性和准确性
1. 化代码问题为符号运算和定理证明问题 :描述准确地反映了符号执行技术的核心理念,即将程序的执行路径转化为符号路径,然后通过逻辑约束来进行推理和验证。这是静态代码分析中常见的方法,用于分析程序可能的执行行为而无需实际运行程序。
2. 使用约束求解算法找到符号解 :这正确地指出了在符号执行中的一个关键步骤,即利用如 SMT (Satisfiability Modulo Theories) 或 SAT (Boolean Satisfiability Problem) 求解器来解决这些约束。如果求解器能够找到满足所有约束的解,这意味着存在一种特定的输入或程序状态,可以使程序执行到某一特定路径。
应用的实用性
3. 把符号解转化成具体的代码位置 :这一步骤非常关键,因为它将抽象的符号结果转化为可以操作的具体信息。例如,在安全性分析中,这可以帮助开发者准确地定位到可能存在漏洞的代码行或路径。
4. 找到 source 和 sink 的交汇点 :在安全性分析中,识别数据从潜在的不安全源(source)流向敏感汇(sink)的路径是至关重要的。这种分析可以帮助识别例如 SQL 注入、跨站脚本(XSS)等常见的安全漏洞。
技术限制
5. 可能无法求解 :这一点正确地指出了符号执行和约束求解中的一个主要挑战,即在某些情况下,由于路径爆炸问题、复杂的约束或资源限制,求解器可能无法找到解或在合理时间内完成求解。
结论
这段描述提供了一个对使用符号执行和约束求解进行代码分析的有效概述。它正确地捕捉了这种技术的工作原理和在实际代码安全性分析中的应用。同时,也简要提到了在实施这种分析时可能遇到的挑战,如复杂性和求解的可行性问题。这种技术是静态代码分析领域的重要组成部分,尤其是在寻求自动化安全审计和缺陷识别方面。

诚如上面提到的关键点:
YAK


构建符号化系统的两层理解



第一层理解:这里如果你要把 有语法有变量甚至有类型的代码 进行符号化的话,其实听起来很没有头绪,但是这个过程有另一个接近的名字,叫“编译”,是 把源码体系编译成另一种符号化的系统体系 ,我们可以认为这个过程是一种“符号化”。
但是既然是两层理解,第二层理解表达了完全不同的路数。如果我们得到的并不是代码,而是 一个“二进制程序” ,或者一段汇编代码,那么针对这一段代码,我们需要 反汇编成新的符号系统(符号化 IR) ,这个过程 有点类似例如 LLVM 做反汇编的案例 。我们发现,反汇编成符号系统也能称之为符号化。
在这两层构建系统的理解中,实际上广泛被人认识的反而是第二种,“反汇编” 成某种 “IR”或者抽象一个题解公式(函数),然后进行 z3(微软出品的某一款约束求解器)求解。关于约束求解的过程,在 CTF 中有各种各样的题目为大家展示,我们就不多叙述了。
这两种理解不论是哪种都并不亲民,而且据我们所知,大部分漏洞并不需要约束求解,甚至很多就是普通的过滤,或者数据流到了危险函数中的参数了,如果 有清晰的数据流 可达性判断,就可以得到正确的结果,并不需求解什么内容。
因为种种主客观原因,对符号系统的约束求解来进行代码审计或者 Fuzz 并不能走入寻常百姓家,这一个部分的玩家一般来说更关注“数理”,而不关心“业务”。

“代码分析”与“图算法“


从数理证明逻辑转变到“业务”逻辑中,我们经常会听到“图”的概念,以至于大家非常乐于尝试直接使用图数据库(Neo4j)来进行代码分析。数据流可以直接变成“图”,由此衍生的图构造方法有很多,比如说关注执行逻辑的,CFG,关注数据流的 Use-Def Chain,所有都关心的 CPG。节点之海也属于这一个范畴。
在这个范畴中,数理运算变得没有那么比重大了,反而图算法(流算法)一些深度或者广度优先算法,甚至洪水算法或者或者连通性算法都直接计算可达性等关键节点关系。
听起来是不是特别完美?从代码抽象成图(或者 AST 抽象成图)的难度,总要比抽象成符号系统要容易得多。
这个结果非常重要,以至于早一开始研究这个领域的时候,我也被这个美好愿景蒙蔽了双眼。实际操作的时候,还是会有很多水土不服的地方:
  1. 可选的跨过程分析需要从某一个节点扩展出去。

  2. OOP 实现中, object.method

    object 往往应该被视为有某种关联的对象。

  3. 闭包噩梦: 在闭包系统中,捕获变量(逃逸变量)可能并不是单纯数据流或者图可以表达得出来的。

  4. ...


但是相对于“数理证明”式的代码分析技术来说,基于“图算法”的算法分析技术已经非常贴近我们对代码分析的理解了。

新的技术方案:SyntaxFlow


在 Yak Project 开始启动“编译原理”的研究之后,我们对代码行为有了更加深入的理解:通过 SSA 格式下的 IR 编译产物,我们可以实现更清晰的数据流认知。因此基于 SSA 格式下的 IR,我们又研发了一个新的“语言”:SyntaxFlow 来描述代码行为,搜索和查询代码行为特征。 不同于 CodeQL 或者某些 Datalog 的模式 ,SyntaxFlow 完全不需要 Import 各种库和表来搜索运算特征。他的使用逻辑 更接近于人 的代码审计过程的逻辑。

YAK


1.编译SSA IR


可以从一个经典的 Java Springboot 的案例来为大家介绍这个非常震撼人心的新技术:
@Controller@RequestMapping("/home/rce")public class RuntimeExec { @RequestMapping("/runtime") public String RuntimeExec(String cmd, Model model) { StringBuilder sb = new StringBuilder(); String line;
try { Process proc = Runtime.getRuntime().exec(cmd);
InputStream fis = proc.getInputStream(); InputStreamReader isr = new InputStreamReader(fis, "GBK"); BufferedReader br = new BufferedReader(isr); while ((line = br.readLine()) != null) { sb.append(line).append(System.lineSeparator()); }
} catch (IOException e) { e.printStackTrace(); sb.append(e); } model.addAttribute("results", sb.toString()); return "basevul/rce/runtime"; }}
我们把这个文件保存在 test.java 中,展示如下的文件夹内容:
❯ tree /tmp/javatest/tmp/javatest└── a1 └── test.java
2 directories, 1 file
一般来说,我们这个文件甚至没有 package ,甚至没有 import ,你要问我这段代码如何审计编译?在比较新的 yak 版本中, 1.3.4-beta3 之后,或者本文编写的最新的主分支中。我们可以使用 yak ssa 命令把代码编译成文件,编译过程会把文件编译成 SSA 的格式,我们可以为这个编译过程设置一个项目名称,让 yaklang 把编译产物存入数据库以方便 SyntaxFlow 进行代码索引和匹配。
❯ yak ssa -t /tmp/javatest --program sf1
通过这个命令,我们把我们的程序存入数据库,编译后的程序名叫 sf1以便我们后续指定程序名进行审计。
YAK


2. 编写 SyntaxFlow 审计语句


在成功把源码进行编译之后,我们如何审计上述代码?仔细观察一下,我们希望审计的最关键的点在:
7| String line; 8| 9| try { 10| Process proc = Runtime.getRuntime().exec(cmd); 11| 12| InputStream fis = proc.getInputStream(); 13| InputStreamReader isr = new InputStreamReader(fis, "GBK");
没错,在第十行有一个 Runtime.getRuntime().exec(cmd) ,我们一般把这个地方会作为 sink。在古早的审计工具中,我们设置 exec 的实际参数们为 sink,设置 Request 为 source,让审计框架替我们去计算 sink 到 source 的可达路径。我们在 SyntaxFlow 的技术中,审计的思路会发生变化,我们认为 exec 的参数部分是关键的数据流,所以我们要先取出来这个参数。那么怎么去编写 SyntaxFlow 规则呢?

基础概念

SyntaxFlow 是一个高级声明式的模式查询语言(Advanced Declarative Pattern Query Language)。不同于 Datalog 类或者 CodeQL,SyntaxFlow 声明的其实是某种代码特征,例如声明 一个函数被调用 时,声明 某个参数或者全部参数 ,声明某一个 数据流的最顶级定义 (产生源),甚至于可以声明 名字是 foobar 的变量有哪些。
例如针对上述的代码,如果我们想要获取,所有 getRuntime 这个函数作为某一个工具类方法的调用,就可以写查询语句为 .getRuntime() 即可。
❯ yak ssa --program sf1 --sf 'getRuntime()'[INFO] 2024-06-13 15:04:18 [ssacli:86] using syntaxflow rule will skip compile[INFO] 2024-06-13 15:04:18 [ssa:38] init ssa database: /Users/v1ll4n/yakit-projects/default-yakssa.db..................[INFO] 2024-06-13 15:04:18 [ssacli:146] syntax flow query result:[INFO] 2024-06-13 15:04:18 [ssacli:148] ===================== Variable:_ ===================[INFO] 2024-06-13 15:04:18 [ssacli:174] /tmp/javatest/a1/test.java:10:35 - 10:47: getRuntime()IR: 335234: Undefined-Runtime.getRuntime(valid)() 7| String line; 8| 9| try { 10| Process proc = Runtime.getRuntime().exec(cmd); 11| 12| InputStream fis = proc.getInputStream(); 13| InputStreamReader isr = new InputStreamReader(fis, "GBK");
通过这个语句的查询,我们可以看到列出了这个地方附近几行上下文代码。

用法列表

SyntaxFlow 的查询操作有很多种,我们可以为大家建立一个表方便用户理解
操作符号
用途说明
基础用法案例
*
通用匹配
单独一个 * 表示全匹配,
*Runtime 表示结尾包含 Runtime 的所有符号或者变量或函数
identifier
按名匹配
直接写 Runtime 意思是匹配所有变量名为 Runtime 的 SSA 符号或者方法为 Runtime 的符号
/regex/
Golang风格的正则匹配
写变量名或者方法或者容器符合正则特征的所有 SSA 符号
.member
以 member 为名的成员(字段或方法都包含)
.getRuntime 表示所有成员包含 getRumtime 为名字的值
.*Runtime ./.*?Runtime/ 正则和 Glob 匹配也是符合要求的
object.member
限定某一个特征的成员调用
foo.bar 表示寻找所有 foo 作为 object,bar 作为成员的调用情况
call()
找到函数调用的指令
getRuntime() 表示所有名字为 getRuntime 的符号被调用的位置。
call(*)
寻找函数调用中的参数审计位置
exec(*) 意思是把 exec 所有的参数都作为审计对象,嵌套从参数开始进行审计。
call(,*,)
从第 N 个参数开始审计,需要用逗号分隔
call(,*,) 表示call这个函数调用的第二个参数开始审计,从第几个逗号开始匹配说明是第几个参数。
->
下一级使用位置
获取审计对象的下一级的使用位置,一般用来做 UD 链的某个位置的下一级用户
-->
最底级使用运算符
获取审计对象的最下级的使用位置,一般用来直接穿透 UD 链
#>
上一级定义位置
获取审计对象的上一级的定义位置,一般用来做 UD 链的某个位置的上一级定义
#->
最顶级定义位置
获取审计对象的最顶级的定义位置,一般用来直接穿透 UD 链到顶端
-{key: value}->
#{key: value}->
带参数控制的顶级底级使用
getRumtime() -{depth: 3}-> 设置一个 深度为 3 的 UD 链递归向下 查询。
as $variable
在语句结束后,暂时保存某一个变量为变量名
exec(* as $sink) 把所有 exec 的参数保存为 $sink 变量。

实战继续

我们构建一个 .getRumtime().exec(* as $params) 的语句,在执行之前,人可以解读出来,审计所有对象包含一个 getRuntime 的成员,获取他的调用指令,在寻找他的调用结果中包含 exec 的成员,再调用 exec 成员,获取 exec 这个函数中所有的参数,把这个参数保存在 $params 中,我们不执行的时候,人脑观察一下,发现这个参数其实是 cmd,cmd 的最顶级的定义是在函数中的。他是一个 “形参(形式参数)”。
接下来我们来验证结果是否符合预期:

❯ yak ssa --program sf1 --sf 'getRuntime().exec(*)'[INFO] 2024-06-13 15:28:43 [ssacli:86] using syntaxflow rule will skip compile[INFO] 2024-06-13 15:28:43 [ssa:38] init ssa database: /Users/v1ll4n/yakit-projects/default-yakssa.db...........................[INFO] 2024-06-13 15:28:43 [ssacli:146] syntax flow query result:






请到「今天看啥」查看全文