写点什么

符号执行,从漏洞扫描到自动化生成测试用例

  • 2021-06-10
  • 本文字数:4031 字

    阅读完需:约 13 分钟

符号执行,从漏洞扫描到自动化生成测试用例

背景

ThoughtWorks 安全团队曾经在可信 Frimware 领域做了一些探索和研究。背景大概是这样的:整车制造过程中,常常会引入供应商的部分设备,如车载娱乐系统,但是出于知识产权的原因,这些供应商很难提供完整的源码给整车制造方,因此二进制的固件就成了整车制造环节中的安全隐患,各种漏洞都可能被供应商的零部件引入,存在于车载系统之中,随时可能被攻击者利用而影响整车的安全性。


为了探测二进制程序中的漏洞,经过一段时间的探索和研究后,把核心技术锁定到了符号执行,利用该技术帮客户搭建了一套自动化的二进制漏洞扫描平台。并且,在后来不断的研究中,我们发现,符号执行也可以用来自动化生成测试用例,为我们更加全面的编写测试用例, 带来新的思路。

什么是符号执行

Wikipedia 上对符号执行的解释:是一种程序分析技术,其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时,该程序会使用符号值作为输入,而非一般执行程序时使用的具体值。在达到目标代码时,分析器可以得到相应的路径约束,然后通过约束求解器来得到可以触发目标代码的具体值。


讲的比较绕,举个通俗的例子来说明:假设程序现在是一个王者荣耀中的英雄,这个英雄经过一定的出装就会有一定的战力(攻速,物理伤害,防御等),符号执行的技术就是,给出了一个英雄的战力,可以反推出什么样的出装可以达到这样的战力。


再举个实际的代码例子来说明符号执行:


void foo(int x, int y){    int t = 0;    if( x > y ){        t = x;    }else{        t = y;    }    if (t < x ){        assert false;    }}
复制代码


假设当t<x时,是我们程序的漏洞,我们要使用符号执行判断是否有达到t<x这个分支的可能。符号执行的方法就是在给定的时间内,生成一组输入,以尽可能多的探索所有的执行路径,在分析时,该程序会使用符号值作为输入,而非具体的值,去探索每一条分支。比如该程序在符号执行完后,会生成如下类似的方程组:


(x>y) => t=x(x<=y) => t=y
复制代码


接下来,符号执行会通过约束求解,去分析上述的每条路径,通过约束求解分析得,如上的两条路径在任何情况下都不可能达到t<x这个分支。约束求解可以简单的理解为解方程,有很多开源的约束求解器,比如 Z3。

使用符号执行进行漏洞扫描

那我们是如何把符号执行运用在自动化漏洞扫描的场景上?


首先要说明的是,我们要扫描的对象是 Linux kernel,对于 kernel 来说有很多已知的 CVE 漏洞,我们的任务就是去发现二进制的 kernel 上是否存在这些 CVE 漏洞。思路如下:

  1. 通过一些简单的逆向,得到该内核的版本。

  2. 有了内核版本,就可以得到内核的源码,以及该内核版本对应的所有 CVE 漏洞和补丁。

  3. 给内核源码打上所有的 CVE 补丁,在二进制层面 diff 前后的补丁,对每个补丁提取唯一的特征(漏洞指纹)。

  4. 用漏洞指纹与目标 kernel 进行对比,扫描得到最终的漏洞列表。


由上述可知,提取漏洞的唯一特征是最重要的一步,接下来介绍如何使用符号执行来提取漏洞指纹。

首先介绍两个基本的概念 BB(basic block)和 CFG(control flow graph):BB 是指从汇编的角度来看程序,一段连续的汇编指令就是一个 BB,这段连续的汇编仅仅包含一个入口和一个出口,换句话说,BB 内部不会有分支和跳转。由此我们可以得出,一个程序,是由一堆的 bb 组成的,它们之间有复杂的调用和跳转关系,最终形成了一张图,这个图就是 CFG。例如下图是一个简单的 CFG:



有了这两个概念,我们就可以对漏洞进行唯一的特征描述了。

漏洞指纹特征

由上面可知,CFG 其实表示了一段程序执行的所有路径,而符号执行的第一步就是去探索所有的执行路径。如果您了解过内核的 CVE 漏洞,就会发现内核很大一部分的 CVE 漏洞补丁,就是在一些关键的代码上加了一些 if 分支和判断。例如 CVE-2019-19252 的补丁如下:


diff --git a/drivers/tty/vt/vc_screen.c b/drivers/tty/vt/vc_screen.cindex 1f042346e7227..778f83ea22493 100644--- a/drivers/tty/vt/vc_screen.c+++ b/drivers/tty/vt/vc_screen.c@@ -456,6 +456,9 @@ vcs_write(struct file *file, const char __user *buf, size_t count, loff_t *ppos)size_t ret;char *con_buf;+ if (use_unicode(inode))+ return -EOPNOTSUPP;+con_buf = (char *) __get_free_page(GFP_KERNEL);if (!con_buf)return -ENOMEM;
复制代码


该补丁只是在 vcs_write 的函数中添加了一个 if 判断,对于这类补丁,在使用符号执行生成 CFG 的时候,前后肯定会出现一个明显的差异,因为多了一个分支,整个的程序流图也就多了一个分支。对于这种类型的补丁,使用 CFG 就可以作为漏洞的特征,通过对比发现,前后的 CFG 不一样,就说明漏洞存在。


那么,仅仅通过 CFG 是否就可以唯一的确定这个漏洞吗?请看下面的 CVE-2019-8956 的例子:


diff --git a/net/sctp/socket.c b/net/sctp/socket.cindex f93c3cf9e5674..65d6d04546aee 100644--- a/net/sctp/socket.c+++ b/net/sctp/socket.c@@ -2027,7 +2027,7 @@ static int sctp_sendmsg(struct sock *sk, struct msghdr *msg, size_t msg_len)struct sctp_endpoint *ep = sctp_sk(sk)->ep;struct sctp_transport *transport = NULL;struct sctp_sndrcvinfo _sinfo, *sinfo;- struct sctp_association *asoc;+ struct sctp_association *asoc, *tmp;struct sctp_cmsgs cmsgs;union sctp_addr *daddr;bool new = false;@@ -2053,7 +2053,7 @@ static int sctp_sendmsg(struct sock *sk, struct msghdr *msg, size_t msg_len)/* SCTP_SENDALL process */if ((sflags & SCTP_SENDALL) && sctp_style(sk, UDP)) {- list_for_each_entry(asoc, &ep->asocs, asocs) {+ list_for_each_entry_safe(asoc, tmp, &ep->asocs, asocs) {err = sctp_sendmsg_check_sflags(asoc, sflags, msg,msg_len);if (err == 0)
复制代码


对于这种漏洞补丁,没有分支上的增减,只是改变了一个函数的入参个数,那么补丁前后的 CFG 可能是一样的,所以我们就不能仅仅通过 CFG 来判断补丁是否存在,必须加上在语义上的分析,语义即这个参数对函数的整体影响。这就引出了符号执行的另一步:约束求解,前面我们提到符号执行会对所有路径形成类似方程组的概念,然后使用约束求解器求出到达每个路径的解的集合。如果其中某些变量发生了改变,其最终的解一定是不一样的,以此作为漏洞标识的另一个特征。

漏洞扫描总结

所以最终,我们是采用符号执行从 CFG 和语义分析两个维度来唯一的确定一个漏洞的特征,然后用这个唯一的特征去目标的 kernel 中对比。以此来确定补丁是否已经存在。这个就是我们检测二进制漏洞的关键技术,大致流程如下图:



在整个过程中,我们会使用开源的符号执行引擎和约束求解器,比如 Angr 和 Z3。

符号执行的其他应用场景

前面是符号执行在漏洞提取和扫描的一个案例,除此之外,符号执行在漏洞挖掘,CTF 等方面也有比较广泛的应用。例如如下程序是我用 Ghidra 逆向的一道 CTF 的题目:


int verify(EVP_PKEY_CTX *ctx, uchar *sig, size_t siglen, uchar *tbs, size_t tbslen){byte bvar1;int local_c;local_c = 0;while(true) {if(ctx[(long)local_c] == (EVP_PKEY_CTX)0x0) {return (int)(uint)(local_c == 0x17);}bVar1 = (byte)local_c;if(encrypted{(long)local_c} != (byte)(((byte)((int)(uint)(bVar1 ^ (byte)ctx[(log)local_c]) \>> (8-((bVar1 ^9)&3) & 0x1f)) | (bVar1 ^ (byte)ctx[(long)local_c]) << ((bVar1 ^9) & 3))+8)){break;}local_c = local_c + 1}return 0;}
复制代码


可以发现,其核心关键是去破解这个加解密的算法(异或,加减等操作),如果人工逆向,可能需要很长时间的推算和尝试,而符号执行则可以自动的去不断尝试每个路径的解,直到算出一个自己需要的值。有兴趣的读者,可以使用 angr 和 z3 去做一下这个 CTF 的破解,非常容易,这里不再赘述。需要说明的是,在破解和 CTF 中,符号执行往往和 IDA/Ghidra 等工具来配合使用。


另一方面是在测试领域,在单元测试中代码覆盖率往往被用于评估代码的测试充分性水平,在软件工业界,人工设计测试用例的方法被广泛使用,即依靠人对程序代码的理解设计测试用例,但对应的人力成本很高,有时候为了降低人力成本且提高自动化程度,随机测试的方法也被常常使用,但一般只能检测到有限的程序行为,容易遗漏软件错误。


在单元测试中,常用的白盒测试的充分性准则大多属于基于控制流的覆盖准则,如语句覆盖,分支覆盖和 MC/DC 覆盖等。而测试准则的选取一般根据实际的测试需求而确定,比如,传统软件的测试一般要求实现尽可能高的语句覆盖和分支覆盖,而对于航天,轨交等控制软件一般要求代码满足 100%的分支覆盖。而这种同时实施多种测试标准的需求,进一步加大了单元测试的工作量和难度, 使得单元测试在实际软件开发中往往被忽略,最终导致软件缺陷没有在早期被及时发现。


而符号执行的特点是会尽可能的遍历每条路径,每一次符号执行的结果等价于大量的测试案例。符号执行为软件的各种情况自动生成了有效的输入,覆盖率高,可以更加容易检测到程序是否存在缺陷和错误。所以,其实我们可以运用符号执行生成测试用例。


目前学术界有不少的论文研究如何使用符号执行自动化生成更好的测试用例。也有一些有意思的 demo,可以让您体验:

C 语言:https://github.com/Sajed49/C-Path-Finder

Java 语言:https://github.com/kaituo/sedge

总结

以上是我们对符号执行的一些探索,欢迎您与我们一起进行更加深入的研究。随着大家对安全的越来越重视,基于符号执行的漏洞扫描,自动测试,fuzz 测试等越来越受到人们的重视。2019 年美国《国防法》National Defense Act 的 H.R.5515—517 就推荐使用二进制分析和符号执行工具来增强关键软件系统的安全。目前,ThoughtWorks 安全团队正在积极探索符号执行在安全领域的威力,通过自动生成测试用例,再结合模糊测试(fuzz)工具,集成到 DevOps 的环境中,在整个软件的开发周期内持续的发现安全漏洞,为软件安全保驾护航。


本文转载自:ThoughtWorks 洞见(ID:TW-Insights)

原文链接:符号执行,从漏洞扫描到自动化生成测试用例

2021-06-10 07:002020

评论

发布
暂无评论
发现更多内容

GAIA数据集V1.10更新

云智慧AIOps社区

运维 AIOPS 数据集

【OpenCV】配置OpenCV教程,OpenCV入门

恒山其若陋兮

5月月更

阿里Java面试必问:JVM与性能优化+Redis+设计模式+分布式

Java浪潮

编程 架构

参与 Apache 顶级开源项目的 N 种方式,Apache Dubbo Samples SIG 成立!

爱好编程进阶

Java 程序员 后端开发

导师男团来袭 | 开源之夏2022,与Alluxio一起探索数据编排的奇妙世界

Alluxio

开源 大学生 #开源项目 开源之夏 数据编排

这么好用的低延时直播,网易云信竟然将它开源了?!

网易云信

开源 WebRTC 音视频技术

再见了收费的Navicat!操作所有数据库有DBeaver就够了

爱好编程进阶

Java 程序员 后端开发

SpringCloud 中 Gateway 是如何关联对应的 GatewayFilterFactory 和 参数解析的

gin

Gateway SpringCould

作为Java程序员连Redis都不会?阿里架构师带你深入“解剖”Redis

Java浪潮

redis JAVA开发 java程序员

分布式事务及其一致性协议

爱好编程进阶

Java 程序员 后端开发

如何制作优秀的产品说明手册?

小炮

产品说明手册

进阶中的程序员:深入解析 Spring boot(含PDF文档分享)

Java浪潮

spring 编程 JAVA开发 springboot

阿联酋航空与华为进一步深化合作伙伴关系

最新动态

微服务网关除了zuul、spring cloud gateway还有更出色的

爱好编程进阶

Java 程序员 后端开发

借鉴这份Java进阶架构师之路的核心知识,我成功收获蚂蚁金服、阿里、美团等Offer

Java浪潮

Java 架构 java架构

字节面试到底有多难,一个Hadoop源码就拦住了百分之90的人群

爱好编程进阶

Java 程序员 后端开发

CRM系统的18个关键功能

低代码小观

CRM 客户关系管理 企业管理系统 CRM系统 客户关系管理系统

黄吉:如何适配OpenHarmony自有音频框架ADM?

OpenHarmony开发者

OpenHarmony

云原生基础治理平台SchedulX V1.2.0正式发布,助力企业降本增效

星汉未来

运维 云原生 星汉未来

Hacker 资讯 | 5 月上旬区块链黑客松活动汇总

One Block Community

区块链

原来,嵌入式BI方案的核心差异全在这,教你如何评估!

葡萄城技术团队

数据分析 BI 嵌入式软件 核心差异

运维审计堡垒机哪款好?报价贵吗?

行云管家

网络安全 堡垒机 IT运维 运维审计

报告解读下载 | 5月《中国数据库行业分析报告》重磅发布!精彩抢先看!

墨天轮

数据库 oracle opengauss TiDB 国产数据库

洞见科技纪凯:基于隐私计算的「客户增长」生态

洞见科技

金融科技 隐私计算

深入浅出Redis丨阿里架构师的Redis实战心得,让你毫不费力的学习

Java浪潮

redis java程序员 java架构

AI简报:Blind超分KernelGAN

AIWeker

人工智能 深度学习 机器视觉 5月月更 超分

网络协议之:memcached binary protocol详解

程序那些事

Java 网络协议 程序那些事 5月月更

[数据分析]-音频分析-BirdCLE-1

浩波的笔记

人工智能 AI 数据分析

手把手推导Back Propagation

OneFlow

人工智能 神经网络 深度学习 Back Propagation 推导过程

毕业总结

凌波微步

架构训练营

堡垒机是服务器吗?两者有区别吗?

行云管家

运维 网络安全 服务器 堡垒机

符号执行,从漏洞扫描到自动化生成测试用例_语言 & 开发_张凯峰_InfoQ精选文章