|
“代码分析”与“数理证明“
在学术圈的代码分析技术(算法)中,我们在这里指的是(在 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 抽象成图)的难度,总要比抽象成符号系统要容易得多。这个结果非常重要,以至于早一开始研究这个领域的时候,我也被这个美好愿景蒙蔽了双眼。实际操作的时候,还是会有很多水土不服的地方:
但是相对于“数理证明”式的代码分析技术来说,基于“图算法”的算法分析技术已经非常贴近我们对代码分析的理解了。
新的技术方案: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:[INFO] 2024-06-13 15:28:43 [ssacli:148] ===================== Variable:_ ===================[INFO] 2024-06-13 15:28:43 [ssacli:174] /tmp/javatest/a1/test.java:5:30 - 5:40: String cmdIR: 335223: Parameter-cmd 2| @RequestMapping("/home/rce") 3| public class RuntimeExec { 4| @RequestMapping("/runtime") 5| public String RuntimeExec(String cmd, Model model) { 6| StringBuilder sb = new StringBuilder(); 7| String line; 8|
我们发现 IR: 335223: Parameter-cmd 成功标志着我们找到了一个名为 cmd 的参数。通过上面的一个审计命令直接关联到了 cmd 的参数。YAK
3.这是碰巧的吗?
用户可能会有点奇怪,这搜索是真的吗?这个例子也未免太简单了一点,那么我们把源码再次进行一些变形。我们去除特别明显的只通过正则就可以匹配到的特征,新增了一些变量传递的过程,那么我们还能生效吗?public class RuntimeExec { @RequestMapping("/runtime") public String RuntimeExec(
String cmd,
Model model) { StringBuilder sb = new StringBuilder(); String line;
try { any runtimeInstance = Runtime.getRuntime(); Process proc = runtimeInstance.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()); }
我们重新编译(yak ssa -t ... --program sf3)之后直接执行上述一样的语句:
❯ yak ssa --program sf3 --sf 'getRuntime().exec(*)'[INFO] 2024-06-13 15:33:55 [ssacli:86] using syntaxflow rule will skip compile[INFO] 2024-06-13 15:33:55 [ssa:38] init ssa database: /Users/v1ll4n/yakit-projects/default-yakssa.db......[INFO] 2024-06-13 15:33:55 [ssacli:146] syntax flow query result:[INFO] 2024-06-13 15:33:55 [ssacli:148] ===================== Variable:_ ===================[INFO] 2024-06-13 15:33:55 [ssacli:174] /tmp/javatest/a1/test.java:8:2 - 8:12: String cmdIR: 335419: Parameter-cmd 5| public String RuntimeExec( 6| 7| 8| String cmd, 9| 10| Model model) { 11| StringBuilder sb = new StringBuilder();
得到了正确的结果,并且还把我修改了源码之后的原样都打印出来了,这个案例足够证明了 SyntaxFlow 是认识数据流的,而不是正则匹配实现的技术。
基于这种技术,我们审计的内容递归起来实际上无关变量,关心的是最底层的数据流流动。
未来已来
SyntaxFlow 的语法和操作序列虽然是全新的,但是他操作的底层元素基本都是我们在“编译拾遗”系列中给大家提到的内容,我们并不是多强力的概念创造者。网络和信息安全领域本质上属于计算机大类的技术分支,在计算机大类中有很多重要的基础工具技术可以解决很多问题,例如我们使用编译技术去实现常见高级语言的 SSA 化,使用精妙的递归编程去编写 Use-Def 链分析算法,使用栈型虚拟机构建分析序列的操作步骤执行。编译原理在通用编程语言的发展中已经获得了十分巨大的进步,这是一个十分完善的学科,我们希望把编译技术带入安全代码分析去分析代码行为,为代码行为分析带来新的机会和可能性。在近期的更新中,我们将会加深 SyntaxFlow 和 SSA IR DB 对常见编程语言的适配,任何人都可以使用 Yak SSA 命令和 SyntaxFlow 进行体验。未来我们也将会在新的产品中展示 SyntaxFlow 的 UI。
|
本帖子中包含更多资源
您需要 登录 才可以下载或查看,没有帐号?立即注册
x
|