背景ThoughtWorks安全团队在可信固件领域做了一些探索和研究。背景大致是这样的：在整车制造过程中，经常会引入一些供应商的设备，比如车载娱乐系统，但由于知识产权的原因，这些供应商很难提供完整的源代码给客户。汽车制造商，因此二进制固件已成为整个汽车制造过程中的安全隐患。供应商的组件可能会引入各种漏洞，并存在于车辆系统中，随时可能被攻击者利用，影响车辆的安全性。为了检测二进制程序中的漏洞，经过一段时间的探索和研究，核心技术锁定在符号执行，并利用该技术帮助客户构建自动化二进制漏洞扫描平台。而且，在后续的不断研究中，我们发现符号执行也可以用于自动生成测试用例，这为我们更全面地编写测试用例带来了新的思路。什么是符号执行维基百科对符号执行的解释：是一种程序分析技术，可以分析程序，得到执行特定代码区域的输入。当使用符号执行分析程序时，程序使用符号值作为输入，而不是通常用于执行程序的具体值。当到达目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器得到能够触发目标代码的具体值。讲的比较绕，我举个通俗的例子来说明：假设现在程序是王者荣耀中的一个英雄，这个英雄经过一定的战斗后会有一定的战力（攻速、物理伤害、防御等）装备数量，象征技的实现就是赋予一个英雄的战力，而什么样的出装才能逆转??达到这样的战力。给出另一个实际的代码示例来说明符号执行：voidfoo(intx,inty){intt=0;if(x>y){t=x;}else{t=y;}if(ty)=>t=x(x<=y)=>t=y接下来，符号执行会求解约束和分析上述每条路径都是通过约束求解来分析的。以上两条路径在任何情况下都不可能实现。使用符号执行进行漏洞扫描。那么我们如何将符号执行应用到自动漏洞扫描的场景中呢？首先，注意我们要扫描的对象是Linux内核。内核有许多已知的CVE漏洞。我们的任务是找出二进制内核中是否存在这些CVE漏洞。思路如下：通过一些简单的逆向工程得到内核的版本。有了内核版本，就可以获得内核的源代码，以及内核版本对应的所有CVE漏洞和补丁。将所有CVE补丁应用到内核源代码中，对二进制级别前后的补丁进行diff，并为每个补丁提取独特的特征（漏洞指纹）。将漏洞指纹与目标内核进行比对，扫描得到最终的漏洞列表。从上面可以看出，提取漏洞的独特特征是最重要的一步。接下来，我们将介绍如何使用符号执行来提取漏洞指纹。首先介绍两个基本概念BB（基本块）和CFG（控制流图）：BB指的是从汇编的角度看程序，一个连续的汇编指令就是一个BB，这个连续的汇编只包含一个入口和一个出口，在其他也就是说，BB里面不会有分支和跳跃。由此我们可以得出一个程序是由一堆bb组成的，它们之间存在着复杂的调用和跳转关系，最后形成一个图，这就是CFG。例如下图是一个简单的CFG：有了这两个概念，我们就可以描述漏洞的独特特征。漏洞指纹特征从上面可以看出，CFG其实代表了一个程序的所有执行路径，而符号执行的第一步就是探索所有的执行路径。如果你了解过内核的CVE漏洞，你会发现内核中很大一部分的CVE漏洞补丁都是在一些关键代码上添加一些if分支和判断。例如CVE-2019-19252的补丁如下：diff--gita/drivers/tty/vt/vc_screen.cb/drivers/tty/vt/vc_screen.cindex1f042346e7227..778f83ea22493100644---a/drivers/tty/vt/vc_screen.C+++b/drivers/tty/vt/vc_screen.c@@-456,6+456,9@@vcs_write(structfile*file,constchar__user*buf,size_tcount,loff_t*ppos)size_tret;char*con_buf;+if(use_unicode(inode))+return-EOPNOTSUPP;+con_buf=(char*)__get_free_page(GFP_KERNEL);if(!con_buf)return-ENOMEM;这个patch只是在vcs_write函数中加入了一个if判断，对于这种Patch，在使用符号执行生成CFG的时候，前后肯定会有明显的区别，因为多了一个分支，整个程序流程图也有一个分支。对于这类补丁，CFG可以作为漏洞的特征。通过对比，发现前后CFG不一样，说明漏洞存在。那么，这个漏洞是否只能由CFG来唯一标识呢？请参见以下CVE-2019-8956示例：diff--gita/net/sctp/socket.cb/net/sctp/socket.cindexf93c3cf9e5674..65d6d04546aee100644---a/net/sctp/socket.c+++b/net/sctp/socket.c@@-2027,7+2027,7@@staticintsctp_sendmsg（structsock*sk，structmsghdr*msg，size_tmsg_len）structsctp_endpoint*ep=sctp_sk（sk）->ep；structsctp_transport*transport=NULL;structsctp_sndrcvinfo_sinfo,*sinfo;-structsctp_association*asoc;+structsctp_association*asoc,*tmp;structsctp_cmsgscmsgs;unionsctp_addr*daddr;boolnew=false;@@7+2053,7@@staticintsctp_sendmsg(structsock*sk,structmsghdr*msg_len_size)tms/*SCTP_SENDALLprocess*/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来判断patch是否存在，必须加上语义分析，语义是指这个参数对功能的整体影响。这导致了符号执行的另一个步骤：约束求解。前面我们提到，符号执行会形成一个类似于所有路径的方程组的概念，然后使用约束求解器找到到达每条路径的解集。如果其中的一些变量发生变化，最终的解决方案一定是不同的，这是漏洞识别的另一个特点。漏洞扫描总结所以最后我们使用符号执行从CFG和语义分析两个维度唯一确定一个漏洞的特征，然后利用这个唯一特征与目标内核进行比较。使用它来确定补丁是否已经存在。这是我们检测二进制漏洞的关键技术。大致流程如下：在整个过程中，我们会使用开源的符号执行引擎和约束求解器，例如Angr和Z3。符号执行的其他应用场景以上是漏洞提取扫描中符号执行的案例。此外，符号执行在漏洞挖掘和CTF中也有广泛的应用。比如下面这个程序是我用Ghidra逆向的一个CTF的标题：intverify(EVP_PKEY_CTX*ctx,uchar*sig,size_tsiglen,uchar*tbs,size_ttbslen){bytebvar1;intlocal_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(加密{(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_clocal_c=local_c+1}return0;}可以发现核心关键是破解加解密算法（XOR、加法、减法等），如果手动逆向，可能需要很长时间计算和尝试，而符号执行可以自动尝试每条路径的解，直到计算出一个你需要的值.有兴趣的读者可以使用angr和z3来破解这个CTF，非常简单，这里不再赘述。需要注意的是，在破解和CTF中，符号执行往往与IDA/Ghidra等工具结合使用。另一方面，在测试领域，代码覆盖率常被用来评价单元测试中代码的测试充分程度。在软件行业中，广泛采用人工设计测试用例的方法，即依靠人对程序代码的理解来设计测试用例，但相应的人工成本较高。有时为了降低人工成本和提高自动化程度，常采用随机测试的方法，但一般只能检测到有限的程序行为，很容易遗漏软件错误。在单元测试中，常用的白盒测试的充分性标准大多属于基于控制流的覆盖标准，如语句覆盖、分支覆盖、MC/DC覆盖等。测试准则的选择一般根据实际测试要求来确定。例如，传统软件的测试一般要求语句覆盖率和分支覆盖率尽可能高，而对于航空航天、轨道交通等控制软件，代码一般要求100%的分支覆盖率。覆盖。需要同时执行多种测试标准，进一步增加了单元测试的工作量和难度，以至于在实际软件开发中往往忽略了单元测试，最终导致软件缺陷在早期无法及时发现。符号执行的特点是尽可能遍历每条路径，每次符号执行的结果相当于大量的测试用例。符号执行针对软件的各种情况自动生成有效输入，覆盖率高，更容易检测程序是否存在缺陷和错误。所以，其实我们可以使用符号执行来生成测试用例。目前，学术界有很多论文介绍如何使用符号执行来自动生成更好的测试用例。还有一些有趣的demo供大家体验：C语言：https://github.com/Sajed49/C-Path-FinderJava语言：https://github.com/kaituo/sedge欢迎大家在-与我们深入研究。随着大家对安全的关注度越来越高，基于符号执行的漏洞扫描、自动测试、模糊测试也越来越受到重视。美国2019年《国防法》国防法案H.R.5515-517建议使用二进制分析和符号执行工具来增强关键软件系统的安全性。【本文为专栏作家《ThoughtWorks》原创稿件，微信公众号：Thinkworker，转载请联系原作者】点此查看该作者更多好文
