符號執行，從漏洞掃描到自動化生成測試用例
背景
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
使用符號執行進行漏洞掃描
那我們是如何把符號執行運用在自動化漏洞掃描的場景上?
首先要說明的是，我們要掃描的對象是Linux kernel，對于kernel來說有很多已知的CVE漏洞，我們的任務就是去發現二進制的kernel上是否存在這些CVE漏洞。思路如下：
- 通過一些簡單的逆向，得到該內核的版本。
- 有了內核版本，就可以得到內核的源碼，以及該內核版本對應的所有CVE漏洞和補丁。
- 給內核源碼打上所有的CVE補丁，在二進制層面diff前后的補丁，對每個補丁提取唯一的特征(漏洞指紋)。
- 用漏洞指紋與目標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.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;
該補丁只是在vcs_write的函數中添加了一個if判斷，對于這類補丁，在使用符號執行生成CFG的時候，前后肯定會出現一個明顯的差異，因為多了一個分支，整個的程序流圖也就多了一個分支。對于這種類型的補丁，使用CFG就可以作為漏洞的特征，通過對比發現，前后的CFG不一樣，就說明漏洞存在。
那么，僅僅通過CFG是否就可以唯一的確定這個漏洞嗎?請看下面的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)
對于這種漏洞補丁，沒有分支上的增減，只是改變了一個函數的入參個數，那么補丁前后的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_clocal_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 就推薦使用二進制分析和符號執行工具來增強關鍵軟件系統的安全。
【本文是51CTO專欄作者“ThoughtWorks”的原創稿件，微信公眾號：思特沃克，轉載請聯系原作者】
