符號(hào)執(zhí)行，從漏洞掃描到自動(dòng)化生成測(cè)試用例
背景
ThoughtWorks安全團(tuán)隊(duì)曾經(jīng)在可信Frimware領(lǐng)域做了一些探索和研究。背景大概是這樣的：整車制造過(guò)程中，常常會(huì)引入供應(yīng)商的部分設(shè)備，如車載娛樂(lè)系統(tǒng)，但是出于知識(shí)產(chǎn)權(quán)的原因，這些供應(yīng)商很難提供完整的源碼給整車制造方，因此二進(jìn)制的固件就成了整車制造環(huán)節(jié)中的安全隱患，各種漏洞都可能被供應(yīng)商的零部件引入，存在于車載系統(tǒng)之中，隨時(shí)可能被攻擊者利用而影響整車的安全性。
為了探測(cè)二進(jìn)制程序中的漏洞，經(jīng)過(guò)一段時(shí)間的探索和研究后，把核心技術(shù)鎖定到了符號(hào)執(zhí)行，利用該技術(shù)幫客戶搭建了一套自動(dòng)化的二進(jìn)制漏洞掃描平臺(tái)。并且，在后來(lái)不斷的研究中，我們發(fā)現(xiàn)，符號(hào)執(zhí)行也可以用來(lái)自動(dòng)化生成測(cè)試用例，為我們更加全面的編寫測(cè)試用例, 帶來(lái)新的思路。
什么是符號(hào)執(zhí)行
Wikipedia上對(duì)符號(hào)執(zhí)行的解釋：是一種程序分析技術(shù)，其可以通過(guò)分析程序來(lái)得到讓特定代碼區(qū)域執(zhí)行的輸入。使用符號(hào)執(zhí)行分析一個(gè)程序時(shí)，該程序會(huì)使用符號(hào)值作為輸入，而非一般執(zhí)行程序時(shí)使用的具體值。在達(dá)到目標(biāo)代碼時(shí)，分析器可以得到相應(yīng)的路徑約束，然后通過(guò)約束求解器來(lái)得到可以觸發(fā)目標(biāo)代碼的具體值。
講的比較繞，舉個(gè)通俗的例子來(lái)說(shuō)明：假設(shè)程序現(xiàn)在是一個(gè)王者榮耀中的英雄，這個(gè)英雄經(jīng)過(guò)一定的出裝就會(huì)有一定的戰(zhàn)力(攻速，物理傷害，防御等)，符號(hào)執(zhí)行的技術(shù)就是，給出了一個(gè)英雄的戰(zhàn)力，可以反推出什么樣的出裝可以達(dá)到這樣的戰(zhàn)力。
再舉個(gè)實(shí)際的代碼例子來(lái)說(shuō)明符號(hào)執(zhí)行：
- void foo(int x, int y)
- {
- int t = 0;
- if( x > y ){
- t = x;
- }else{
- t = y;
- }
- if (t < x ){
- assert false;
- }
- }
假設(shè)當(dāng)t<x時(shí)，是我們程序的漏洞，我們要使用符號(hào)執(zhí)行判斷是否有達(dá)到t<x這個(gè)分支的可能。符號(hào)執(zhí)行的方法就是在給定的時(shí)間內(nèi)，生成一組輸入，以盡可能多的探索所有的執(zhí)行路徑，在分析時(shí)，該程序會(huì)使用符號(hào)值作為輸入，而非具體的值，去探索每一條分支。比如該程序在符號(hào)執(zhí)行完后，會(huì)生成如下類似的方程組：
- (x>y) => t=x
- (x<=y) => t=y
接下來(lái)，符號(hào)執(zhí)行會(huì)通過(guò)約束求解，去分析上述的每條路徑，通過(guò)約束求解分析得，如上的兩條路徑在任何情況下都不可能達(dá)到t
使用符號(hào)執(zhí)行進(jìn)行漏洞掃描
那我們是如何把符號(hào)執(zhí)行運(yùn)用在自動(dòng)化漏洞掃描的場(chǎng)景上?
首先要說(shuō)明的是，我們要掃描的對(duì)象是Linux kernel，對(duì)于kernel來(lái)說(shuō)有很多已知的CVE漏洞，我們的任務(wù)就是去發(fā)現(xiàn)二進(jìn)制的kernel上是否存在這些CVE漏洞。思路如下：
- 通過(guò)一些簡(jiǎn)單的逆向，得到該內(nèi)核的版本。
- 有了內(nèi)核版本，就可以得到內(nèi)核的源碼，以及該內(nèi)核版本對(duì)應(yīng)的所有CVE漏洞和補(bǔ)丁。
- 給內(nèi)核源碼打上所有的CVE補(bǔ)丁，在二進(jìn)制層面diff前后的補(bǔ)丁，對(duì)每個(gè)補(bǔ)丁提取唯一的特征(漏洞指紋)。
- 用漏洞指紋與目標(biāo)kernel進(jìn)行對(duì)比，掃描得到最終的漏洞列表。
由上述可知，提取漏洞的唯一特征是最重要的一步，接下來(lái)介紹如何使用符號(hào)執(zhí)行來(lái)提取漏洞指紋。
首先介紹兩個(gè)基本的概念BB(basic block)和CFG(control flow graph):BB是指從匯編的角度來(lái)看程序，一段連續(xù)的匯編指令就是一個(gè)BB，這段連續(xù)的匯編僅僅包含一個(gè)入口和一個(gè)出口，換句話說(shuō)，BB內(nèi)部不會(huì)有分支和跳轉(zhuǎn)。由此我們可以得出，一個(gè)程序，是由一堆的bb組成的，它們之間有復(fù)雜的調(diào)用和跳轉(zhuǎn)關(guān)系，最終形成了一張圖，這個(gè)圖就是CFG。例如下圖是一個(gè)簡(jiǎn)單的CFG：
有了這兩個(gè)概念，我們就可以對(duì)漏洞進(jìn)行唯一的特征描述了。
漏洞指紋特征
由上面可知，CFG其實(shí)表示了一段程序執(zhí)行的所有路徑，而符號(hào)執(zhí)行的第一步就是去探索所有的執(zhí)行路徑。如果您了解過(guò)內(nèi)核的CVE漏洞，就會(huì)發(fā)現(xiàn)內(nèi)核很大一部分的CVE漏洞補(bǔ)丁，就是在一些關(guān)鍵的代碼上加了一些if分支和判斷。例如CVE-2019-19252的補(bǔ)丁如下：
- diff --git a/drivers/tty/vt/vc_screen.c b/drivers/tty/vt/vc_screen.c
- index 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;
該補(bǔ)丁只是在vcs_write的函數(shù)中添加了一個(gè)if判斷，對(duì)于這類補(bǔ)丁，在使用符號(hào)執(zhí)行生成CFG的時(shí)候，前后肯定會(huì)出現(xiàn)一個(gè)明顯的差異，因?yàn)槎嗔艘粋€(gè)分支，整個(gè)的程序流圖也就多了一個(gè)分支。對(duì)于這種類型的補(bǔ)丁，使用CFG就可以作為漏洞的特征，通過(guò)對(duì)比發(fā)現(xiàn)，前后的CFG不一樣，就說(shuō)明漏洞存在。
那么，僅僅通過(guò)CFG是否就可以唯一的確定這個(gè)漏洞嗎?請(qǐng)看下面的CVE-2019-8956的例子：
- diff --git a/net/sctp/socket.c b/net/sctp/socket.c
- index 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)
對(duì)于這種漏洞補(bǔ)丁，沒有分支上的增減，只是改變了一個(gè)函數(shù)的入?yún)€(gè)數(shù)，那么補(bǔ)丁前后的CFG可能是一樣的，所以我們就不能僅僅通過(guò)CFG來(lái)判斷補(bǔ)丁是否存在，必須加上在語(yǔ)義上的分析，語(yǔ)義即這個(gè)參數(shù)對(duì)函數(shù)的整體影響。這就引出了符號(hào)執(zhí)行的另一步：約束求解，前面我們提到符號(hào)執(zhí)行會(huì)對(duì)所有路徑形成類似方程組的概念，然后使用約束求解器求出到達(dá)每個(gè)路徑的解的集合。如果其中某些變量發(fā)生了改變，其最終的解一定是不一樣的，以此作為漏洞標(biāo)識(shí)的另一個(gè)特征。
漏洞掃描總結(jié)
所以最終，我們是采用符號(hào)執(zhí)行從CFG和語(yǔ)義分析兩個(gè)維度來(lái)唯一的確定一個(gè)漏洞的特征，然后用這個(gè)唯一的特征去目標(biāo)的kernel中對(duì)比。以此來(lái)確定補(bǔ)丁是否已經(jīng)存在。這個(gè)就是我們檢測(cè)二進(jìn)制漏洞的關(guān)鍵技術(shù)，大致流程如下圖：
在整個(gè)過(guò)程中，我們會(huì)使用開源的符號(hào)執(zhí)行引擎和約束求解器，比如Angr和Z3。
符號(hào)執(zhí)行的其他應(yīng)用場(chǎng)景
前面是符號(hào)執(zhí)行在漏洞提取和掃描的一個(gè)案例，除此之外，符號(hào)執(zhí)行在漏洞挖掘，CTF等方面也有比較廣泛的應(yīng)用。例如如下程序是我用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_clocal_c = local_c + 1
- }
- return 0;
- }
可以發(fā)現(xiàn)，其核心關(guān)鍵是去破解這個(gè)加解密的算法(異或，加減等操作)，如果人工逆向，可能需要很長(zhǎng)時(shí)間的推算和嘗試，而符號(hào)執(zhí)行則可以自動(dòng)的去不斷嘗試每個(gè)路徑的解，直到算出一個(gè)自己需要的值。有興趣的讀者，可以使用angr和z3去做一下這個(gè)CTF的破解，非常容易，這里不再贅述。需要說(shuō)明的是，在破解和CTF中，符號(hào)執(zhí)行往往和IDA/Ghidra等工具來(lái)配合使用。
另一方面是在測(cè)試領(lǐng)域，在單元測(cè)試中代碼覆蓋率往往被用于評(píng)估代碼的測(cè)試充分性水平，在軟件工業(yè)界，人工設(shè)計(jì)測(cè)試用例的方法被廣泛使用，即依靠人對(duì)程序代碼的理解設(shè)計(jì)測(cè)試用例，但對(duì)應(yīng)的人力成本很高，有時(shí)候?yàn)榱私档腿肆Τ杀厩姨岣咦詣?dòng)化程度，隨機(jī)測(cè)試的方法也被常常使用，但一般只能檢測(cè)到有限的程序行為，容易遺漏軟件錯(cuò)誤。
在單元測(cè)試中，常用的白盒測(cè)試的充分性準(zhǔn)則大多屬于基于控制流的覆蓋準(zhǔn)則，如語(yǔ)句覆蓋，分支覆蓋和MC/DC覆蓋等。而測(cè)試準(zhǔn)則的選取一般根據(jù)實(shí)際的測(cè)試需求而確定，比如，傳統(tǒng)軟件的測(cè)試一般要求實(shí)現(xiàn)盡可能高的語(yǔ)句覆蓋和分支覆蓋，而對(duì)于航天，軌交等控制軟件一般要求代碼滿足100%的分支覆蓋。而這種同時(shí)實(shí)施多種測(cè)試標(biāo)準(zhǔn)的需求，進(jìn)一步加大了單元測(cè)試的工作量和難度， 使得單元測(cè)試在實(shí)際軟件開發(fā)中往往被忽略，最終導(dǎo)致軟件缺陷沒有在早期被及時(shí)發(fā)現(xiàn)。
而符號(hào)執(zhí)行的特點(diǎn)是會(huì)盡可能的遍歷每條路徑，每一次符號(hào)執(zhí)行的結(jié)果等價(jià)于大量的測(cè)試案例。符號(hào)執(zhí)行為軟件的各種情況自動(dòng)生成了有效的輸入，覆蓋率高，可以更加容易檢測(cè)到程序是否存在缺陷和錯(cuò)誤。所以，其實(shí)我們可以運(yùn)用符號(hào)執(zhí)行生成測(cè)試用例。
目前學(xué)術(shù)界有不少的論文研究如何使用符號(hào)執(zhí)行自動(dòng)化生成更好的測(cè)試用例。也有一些有意思的demo，可以讓您體驗(yàn)：
- C語(yǔ)言：https://github.com/Sajed49/C-Path-Finder
- Java語(yǔ)言：https://github.com/kaituo/sedge
總結(jié)
以上是我們對(duì)符號(hào)執(zhí)行的一些探索，歡迎您與我們一起進(jìn)行更加深入的研究。隨著大家對(duì)安全的越來(lái)越重視，基于符號(hào)執(zhí)行的漏洞掃描，自動(dòng)測(cè)試，fuzz測(cè)試等越來(lái)越受到人們的重視。2019年美國(guó)《國(guó)防法》National Defense Act的H.R.5515—517 就推薦使用二進(jìn)制分析和符號(hào)執(zhí)行工具來(lái)增強(qiáng)關(guān)鍵軟件系統(tǒng)的安全。
【本文是51CTO專欄作者“ThoughtWorks”的原創(chuàng)稿件，微信公眾號(hào)：思特沃克，轉(zhuǎn)載請(qǐng)聯(lián)系原作者】
