輔助檢測(cè)Linux驅(qū)動(dòng)中漏洞的符號(hào)驅(qū)動(dòng)環(huán)境*

范文良，茅俊杰，肖奇學(xué)，徐永健，楊維康，陳渝

(清華大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系，北京 100084)

摘要：Linux系統(tǒng)中的驅(qū)動(dòng)漏洞被證實(shí)是內(nèi)核漏洞的主要來(lái)源，可以被利用導(dǎo)致嚴(yán)重的安全問(wèn)題。通過(guò)系統(tǒng)模型、驅(qū)動(dòng)與內(nèi)核的交互和驅(qū)動(dòng)與設(shè)備的交互這三部分的設(shè)計(jì)與實(shí)現(xiàn)，構(gòu)建了符號(hào)驅(qū)動(dòng)環(huán)境，用于輔助檢測(cè)Linux驅(qū)動(dòng)中的漏洞。使用符號(hào)驅(qū)動(dòng)環(huán)境對(duì)兩個(gè)真實(shí)的驅(qū)動(dòng)進(jìn)行檢測(cè)，成功檢測(cè)出了兩個(gè)漏洞，證實(shí)了該工具的可行性。與SymDrive工具的性能相比，符號(hào)驅(qū)動(dòng)環(huán)境執(zhí)行速度快90%，覆蓋率提高20%。

關(guān)鍵詞：驅(qū)動(dòng)漏洞；漏洞檢測(cè)；符號(hào)執(zhí)行；驅(qū)動(dòng)環(huán)境

中圖分類號(hào)：TP309.2 文獻(xiàn)標(biāo)志碼：A

doi:10.3969/j.issn.1007-130X.2015.06.005

收稿日期：*2014-05-05;修回日期：2014-06-11

基金項(xiàng)目：國(guó)家自然科學(xué)基金資助項(xiàng)目(61170050)；核高基重大專項(xiàng)基金資助項(xiàng)目(2012ZX01039-004)

作者簡(jiǎn)介:

通信地址：100084 北京市清華大學(xué)FIT樓3-124

Address:Room 3-124,FIT Building,Tsinghua University,Beijing 100084,P.R.China

Symbolicdriverenvironment:atoolaidedtodetectLinuxdriverbugs

FANWen-liang,MAOJun-jie,XIAOQi-xue,XUYong-jian,YANGWei-kang,CHENYu

(DepartmentofComputerScienceandTechnology,TsinghuaUniversity,Beijing100084,China)

Abstract:It has been proved that Linux driver bugs are the major bug source of the whole system, which can lead to serious security problems.A tool called symbolic driver environment (SDE) is designed to detect Linux driver bugs, which consists of the system model,the interactions between driver and kernel, and the interactions between driver and device.Using SDE, we detect two real Linux drivers, and find two bugs. The results prove that the tool is feasible, and the speed is 90% faster and the coverage is 20% larger compared with an existing tool called SymDrive.

Keywords:driverbugs;detectbugs;symbolicexecution;driverenvironment

1引言

Linux是一個(gè)使用廣泛的開(kāi)源操作系統(tǒng)，由于每個(gè)用戶都可以獲得并分析Linux的源代碼，再加上近年來(lái)Android系統(tǒng)(基于Linux)在移動(dòng)端廣泛使用，使得Linux系統(tǒng)的安全性面臨著重大的挑戰(zhàn)。近來(lái)很多研究表明，內(nèi)核驅(qū)動(dòng)程序(簡(jiǎn)稱驅(qū)動(dòng))是內(nèi)核漏洞的主要制造者。斯坦福大學(xué)的一項(xiàng)研究表明[1]，Linux驅(qū)動(dòng)中的漏洞要比內(nèi)核中的其余部分多3～7倍。在另一流行的操作系統(tǒng)Windows中，也有研究表明[2]，有27%的系統(tǒng)崩潰是由驅(qū)動(dòng)所引起的，相比之下由內(nèi)核本身引起的只有2%。這些都證明了安全驅(qū)動(dòng)的重要性。

驅(qū)動(dòng)中的漏洞類型有硬件依賴錯(cuò)誤、API誤用、競(jìng)爭(zhēng)、申請(qǐng)釋放不匹配、內(nèi)存泄露、驅(qū)動(dòng)接口誤用、指針問(wèn)題等。現(xiàn)有的漏洞檢測(cè)工具主要分為：靜態(tài)分析工具、符號(hào)執(zhí)行工具和動(dòng)態(tài)分析工具。使用現(xiàn)有的工具檢測(cè)驅(qū)動(dòng)中的漏洞存在以下問(wèn)題：

(1)觀測(cè)性：驅(qū)動(dòng)誤用內(nèi)核接口的真正位置很難檢測(cè)，這是由于大多數(shù)驅(qū)動(dòng)對(duì)內(nèi)核接口的誤用不會(huì)立即導(dǎo)致系統(tǒng)崩潰，而是使系統(tǒng)處于不穩(wěn)定的狀態(tài)，在之后引發(fā)崩潰或異常行為。

(2)覆蓋率：驅(qū)動(dòng)中的漏洞通常會(huì)發(fā)生在一些很少見(jiàn)的狀態(tài)中，傳統(tǒng)的測(cè)試工具通常無(wú)法覆蓋到這些狀態(tài)，也就無(wú)法檢測(cè)出這些漏洞。

針對(duì)上述問(wèn)題，本文首先介紹了用于漏洞檢測(cè)的三種主要方法：靜態(tài)分析、符號(hào)執(zhí)行和動(dòng)態(tài)分析。然后，綜合上述方法的特點(diǎn)，提出了輔助檢測(cè)Linux驅(qū)動(dòng)中漏洞的原型系統(tǒng)——符號(hào)驅(qū)動(dòng)環(huán)境，改進(jìn)了靜態(tài)分析誤報(bào)率高，動(dòng)態(tài)分析依賴輸入、難以定位漏洞位置、符號(hào)執(zhí)行會(huì)引起路徑爆炸的問(wèn)題。最后，通過(guò)將符號(hào)驅(qū)動(dòng)環(huán)境應(yīng)用于Linux中的lp打印機(jī)驅(qū)動(dòng)和e100網(wǎng)卡驅(qū)動(dòng)，檢測(cè)出兩個(gè)真實(shí)存在的漏洞，驗(yàn)證了該原型系統(tǒng)的可行性，并通過(guò)與SymDrive的對(duì)比，表明了符號(hào)驅(qū)動(dòng)環(huán)境執(zhí)行速度更快，覆蓋率更高。

2相關(guān)工作

2.1靜態(tài)分析

靜態(tài)分析是指在不運(yùn)行代碼的方式下，通過(guò)詞法分析、語(yǔ)法分析、控制流分析等技術(shù)對(duì)程序代碼進(jìn)行掃描，驗(yàn)證代碼是否滿足規(guī)范性、安全性、可靠性、可維護(hù)性等指標(biāo)的一種代碼分析技術(shù)，近來(lái)靜態(tài)分析越來(lái)越多地被應(yīng)用到漏洞檢測(cè)領(lǐng)域。靜態(tài)分析十分快速，但誤報(bào)率較高。靜態(tài)分析工具有：麻省理工學(xué)院開(kāi)發(fā)的KINT[3]，用于檢測(cè)C語(yǔ)言源碼中的整數(shù)溢出漏洞；伯克利大學(xué)開(kāi)發(fā)的BLAST[4]，用于解決C語(yǔ)言源碼中的可達(dá)性問(wèn)題，即如何從程序入口點(diǎn)到達(dá)程序中的給定點(diǎn)；微軟公司開(kāi)發(fā)的SDV(StaticDriverVerifier)[5]，用于檢測(cè)Windows驅(qū)動(dòng)中的內(nèi)核接口的正確使用。

SDV具有典型的代表性，其主要包括Windows系統(tǒng)的模型及驅(qū)動(dòng)運(yùn)行的模擬環(huán)境以及60余條內(nèi)核接口的使用規(guī)則。SDV在系統(tǒng)模型中模擬運(yùn)行驅(qū)動(dòng)源碼，在內(nèi)核接口中通過(guò)規(guī)則檢測(cè)對(duì)其的正確使用，最后輸出錯(cuò)誤報(bào)告。SDV通過(guò)檢測(cè)規(guī)則來(lái)定義內(nèi)核接口的正確使用，從而解決了驅(qū)動(dòng)檢測(cè)中觀測(cè)性的問(wèn)題。

微軟公司使用SDV對(duì)大量驅(qū)動(dòng)進(jìn)行了檢測(cè)并發(fā)現(xiàn)了120余個(gè)嚴(yán)重的漏洞，但SDV仍存在如下問(wèn)題：首先，SDV是一個(gè)閉源工具，無(wú)法將其移植用于檢測(cè)Linux驅(qū)動(dòng)中漏洞；其次，SDV限于靜態(tài)分析，難以分析函數(shù)指針以及用于內(nèi)存檢測(cè)等；最后，SDV雖能夠覆蓋到驅(qū)動(dòng)調(diào)用內(nèi)核接口失敗的情況，但是對(duì)驅(qū)動(dòng)中由于設(shè)備輸入而引起的分支情況覆蓋率很低。

2.2符號(hào)執(zhí)行

符號(hào)執(zhí)行技術(shù)在程序分析和漏洞檢測(cè)方面有著廣泛的應(yīng)用，其原理是用符號(hào)作為輸入，對(duì)程序進(jìn)行解釋執(zhí)行，以此枚舉出程序所有可能的執(zhí)行情況。在解釋執(zhí)行的過(guò)程中，執(zhí)行引擎將所有變量對(duì)應(yīng)為一個(gè)包含代數(shù)運(yùn)算及內(nèi)存訪問(wèn)的表達(dá)式，表示該變量與輸入符號(hào)的關(guān)系；當(dāng)變量用于條件判斷時(shí)，執(zhí)行引擎枚舉該條件為真和為假的兩條分支路徑，在每條路徑上記錄其被執(zhí)行的條件(稱為“路徑約束”)，并獨(dú)立地繼續(xù)執(zhí)行這兩條路徑。當(dāng)需要給變量指定具體值時(shí)，使用求解器對(duì)約束表達(dá)式進(jìn)行求解。符號(hào)執(zhí)行舉例如圖1所示。

Figure 1　Example of symbolic execution 圖1　符號(hào)執(zhí)行例子

設(shè)x為符號(hào)值，在遇到x<5這一分支判斷時(shí)，執(zhí)行引擎會(huì)分支并形成兩條路徑，一條路徑關(guān)于x的約束表達(dá)式是x<5，該路徑繼續(xù)執(zhí)行判斷體內(nèi)的語(yǔ)句；另一條路徑關(guān)于x的約束表達(dá)式是x≥5，該路徑跳過(guò)判斷體繼續(xù)執(zhí)行。判斷體中的x<0同理。設(shè)sysFn函數(shù)中要輸出x的值，求解器就會(huì)在x<5這一范圍內(nèi)給x賦隨機(jī)值，比如0。

符號(hào)執(zhí)行工具有：洛桑理工學(xué)院開(kāi)發(fā)的S2E(SelectiveSymbolicExecution)[6]，是用于符號(hào)執(zhí)行二進(jìn)制代碼的虛擬機(jī)；斯坦福大學(xué)開(kāi)發(fā)的KLEE[7]，是用于解釋執(zhí)行LLVM[8]中間代碼的平臺(tái)。KLEE是具有代表性的符號(hào)執(zhí)行引擎，使用執(zhí)行狀態(tài)來(lái)表示程序運(yùn)行過(guò)程中某一時(shí)刻的狀態(tài)，每一條執(zhí)行狀態(tài)代表一條路徑，KLEE解釋執(zhí)行LLVM中間代碼的過(guò)程實(shí)際就是執(zhí)行狀態(tài)發(fā)生變化的過(guò)程。KLEE只能對(duì)鏈接生成的目標(biāo)文件進(jìn)行符號(hào)執(zhí)行分析，因此無(wú)法符號(hào)執(zhí)行Linux系統(tǒng)，從而無(wú)法符號(hào)執(zhí)行依賴于操作系統(tǒng)的Linux驅(qū)動(dòng)。符號(hào)執(zhí)行覆蓋率很高，但是存在路徑爆炸的問(wèn)題：即路徑數(shù)目呈指數(shù)型增長(zhǎng)，最后導(dǎo)致內(nèi)存耗盡。KLEE提供了一些限制手段來(lái)防止路徑爆炸，如限制路徑深度、限制最大路徑分支數(shù)等。

2.3動(dòng)態(tài)分析

動(dòng)態(tài)分析是指在運(yùn)行時(shí)監(jiān)控程序行為、收集程序信息進(jìn)行漏洞檢測(cè)，一般通過(guò)構(gòu)造特定的輸入來(lái)觸發(fā)漏洞。動(dòng)態(tài)分析可以解決靜態(tài)分析很難解決的問(wèn)題，如指針、內(nèi)存檢測(cè)等，但動(dòng)態(tài)分析需要很大的工作量來(lái)構(gòu)造輸入，由于觀測(cè)性的問(wèn)題，動(dòng)態(tài)分析也很難定位驅(qū)動(dòng)中漏洞的位置。動(dòng)態(tài)分析往往和別的分析方法綜合使用，檢測(cè)效果較好的工具有：洛桑理工學(xué)院基于S2E開(kāi)發(fā)的DDT[9]，用于檢測(cè)Windows網(wǎng)卡驅(qū)動(dòng)中的漏洞；威斯康辛大學(xué)基于S2E開(kāi)發(fā)的SymDrive[10]，用于檢測(cè)Linux驅(qū)動(dòng)中的多種漏洞。

SymDrive的總體結(jié)構(gòu)見(jiàn)圖2。SymDrive是源碼級(jí)的工具，首先使用源碼轉(zhuǎn)換工具CIL[11]對(duì)驅(qū)動(dòng)源碼進(jìn)行插樁，來(lái)輔助動(dòng)態(tài)符號(hào)執(zhí)行，然后使用符號(hào)化設(shè)備來(lái)模擬硬件產(chǎn)生的輸入，最后將驅(qū)動(dòng)運(yùn)行在QEMU虛擬機(jī)中執(zhí)行檢測(cè)。SymDrive提出并實(shí)現(xiàn)了符號(hào)化設(shè)備這一思想，其原理如下：首先，虛擬機(jī)可以發(fā)現(xiàn)并配置虛擬的符號(hào)化設(shè)備，然后加載合適的驅(qū)動(dòng)；其次，當(dāng)驅(qū)動(dòng)需要設(shè)備提供輸入時(shí)，符號(hào)化設(shè)備可以產(chǎn)生一系列符號(hào)值，來(lái)輔助驅(qū)動(dòng)的符號(hào)執(zhí)行，達(dá)到高覆蓋率測(cè)試的目的。SymDrive的檢測(cè)依賴CIL的源碼插樁，通過(guò)在驅(qū)動(dòng)的源代碼中插入一些相應(yīng)的規(guī)則，在動(dòng)態(tài)執(zhí)行到該檢測(cè)點(diǎn)時(shí)驗(yàn)證當(dāng)前路徑能否通過(guò)該檢測(cè)。這種檢測(cè)方式比較準(zhǔn)確，但由于其真實(shí)地執(zhí)行代碼，會(huì)花費(fèi)大量的時(shí)間在內(nèi)核執(zhí)行上，所以執(zhí)行時(shí)間通常很長(zhǎng)；另外，由于符號(hào)化設(shè)備會(huì)產(chǎn)生大量的符號(hào)值，經(jīng)常會(huì)造成路徑爆炸，SymDrive提供了注釋插件來(lái)規(guī)避這一問(wèn)題。

Figure 2　Architecture of SymDrive 圖2　SymDrive總體結(jié)構(gòu)

3符號(hào)驅(qū)動(dòng)環(huán)境

本文在SymDrive的符號(hào)化設(shè)備和KLEE符號(hào)執(zhí)行的基礎(chǔ)上，實(shí)現(xiàn)了符號(hào)驅(qū)動(dòng)環(huán)境——輔助檢測(cè)Linux驅(qū)動(dòng)中漏洞的工具。符號(hào)驅(qū)動(dòng)環(huán)境使用符號(hào)執(zhí)行改進(jìn)了SDV覆蓋率低的問(wèn)題，使用Linux系統(tǒng)模型解決了無(wú)法在KLEE中執(zhí)行驅(qū)動(dòng)的問(wèn)題，使用內(nèi)核接口和改進(jìn)的符號(hào)化設(shè)備改進(jìn)了SymDrive執(zhí)行時(shí)間長(zhǎng)和路徑爆炸的問(wèn)題。在符號(hào)驅(qū)動(dòng)環(huán)境上可以通過(guò)定制系統(tǒng)行為來(lái)模擬驅(qū)動(dòng)功能、支持不同類型驅(qū)動(dòng)，以及添加檢測(cè)規(guī)則來(lái)檢測(cè)多種類型的漏洞。符號(hào)驅(qū)動(dòng)環(huán)境的設(shè)計(jì)目的是為L(zhǎng)inux驅(qū)動(dòng)提供一個(gè)輕量級(jí)的運(yùn)行環(huán)境，更充分地測(cè)試驅(qū)動(dòng)代碼，減少內(nèi)核代碼的執(zhí)行時(shí)間，從而減少測(cè)試時(shí)間，提高代碼覆蓋率。

符號(hào)驅(qū)動(dòng)環(huán)境具備以下特點(diǎn)：

(1)可定制性：不同類型的驅(qū)動(dòng)的功能各不相同，如網(wǎng)卡驅(qū)動(dòng)可用于發(fā)包、收包、查詢網(wǎng)絡(luò)參數(shù)，LED驅(qū)動(dòng)可用于控制LED燈的亮、暗等。符號(hào)驅(qū)動(dòng)環(huán)境通過(guò)系統(tǒng)模型管理操作系統(tǒng)主動(dòng)調(diào)用驅(qū)動(dòng)的流程，用戶可以簡(jiǎn)單地通過(guò)定制系統(tǒng)模型來(lái)模擬驅(qū)動(dòng)的功能，實(shí)現(xiàn)對(duì)不同類型驅(qū)動(dòng)的支持，提高對(duì)驅(qū)動(dòng)代碼測(cè)試的覆蓋率。

(2)可擴(kuò)展性：符號(hào)驅(qū)動(dòng)環(huán)境通過(guò)規(guī)則來(lái)檢測(cè)漏洞，不同類型的漏洞需要有不同的檢測(cè)規(guī)則，本文在符號(hào)驅(qū)動(dòng)環(huán)境中添加了常見(jiàn)的如內(nèi)存、鎖等方面的檢測(cè)規(guī)則。符號(hào)驅(qū)動(dòng)環(huán)境還可以添加更多的檢測(cè)規(guī)則，從而實(shí)現(xiàn)對(duì)更多類型漏洞的檢測(cè)，提高了整個(gè)工具的擴(kuò)展性。

符號(hào)驅(qū)動(dòng)環(huán)境的結(jié)構(gòu)如圖3所示。符號(hào)驅(qū)動(dòng)環(huán)境主要分為系統(tǒng)模型、驅(qū)動(dòng)與內(nèi)核的交互以及驅(qū)動(dòng)與設(shè)備的交互三部分，其執(zhí)行流程如下：首先，通過(guò)系統(tǒng)模型來(lái)主動(dòng)調(diào)用驅(qū)動(dòng)；然后，當(dāng)驅(qū)動(dòng)執(zhí)行到內(nèi)核接口時(shí)，通過(guò)簡(jiǎn)化的內(nèi)核實(shí)現(xiàn)來(lái)完成相應(yīng)的功能并執(zhí)行檢測(cè)；之后，當(dāng)驅(qū)動(dòng)需要與設(shè)備交互時(shí)，通過(guò)符號(hào)化設(shè)備來(lái)完成交互；最后，完成系統(tǒng)模型的調(diào)用邏輯之后，輸出錯(cuò)誤報(bào)告并使用求解器求解出可以觸發(fā)漏洞的相關(guān)輸入的具體值。

Figure 3　Architecture of symboilc driver environment 圖3　符號(hào)驅(qū)動(dòng)環(huán)境總體結(jié)構(gòu)

3.1系統(tǒng)模型

系統(tǒng)模型用于模擬Linux系統(tǒng)對(duì)驅(qū)動(dòng)調(diào)用的流程和完成驅(qū)動(dòng)功能(如觸發(fā)網(wǎng)卡驅(qū)動(dòng)收包)，以達(dá)到可定制地執(zhí)行各種類型驅(qū)動(dòng)的目的。每一種類型的驅(qū)動(dòng)都有其固定的調(diào)用模式，這一模式也反映在每類驅(qū)動(dòng)都有一些固定的函數(shù)指針上，如表1所示(以e100網(wǎng)卡驅(qū)動(dòng)為例)。

Table 1　 Some function pointers in e100 net driver( part)

下邊以e100網(wǎng)卡驅(qū)動(dòng)為例，說(shuō)明定制了收、發(fā)包功能的系統(tǒng)模型的調(diào)用模式：首先，通過(guò)module_init()暴露的驅(qū)動(dòng)函數(shù)開(kāi)啟驅(qū)動(dòng)的注冊(cè)，并調(diào)用probe和open函數(shù)指針完成驅(qū)動(dòng)的注冊(cè)；然后，調(diào)用ndo_start_xmit函數(shù)指針模擬實(shí)現(xiàn)發(fā)包的功能，模擬硬中斷觸發(fā)收包，調(diào)用驅(qū)動(dòng)注冊(cè)的中斷處理函數(shù)完成收包的操作；最后，以與注冊(cè)相反的順序，調(diào)用close、remove函數(shù)指針和module_exit()暴露的函數(shù)來(lái)注銷驅(qū)動(dòng)。

以上就是定制了收、發(fā)包功能的網(wǎng)卡驅(qū)動(dòng)的調(diào)用模式，這一調(diào)用模式能覆蓋50%左右的網(wǎng)卡驅(qū)動(dòng)函數(shù)，包括注冊(cè)中讀取設(shè)備配置信息等函數(shù)，發(fā)包、收包的主要函數(shù)，以及注銷中釋放內(nèi)存、垃圾回收等函數(shù)。用戶可以通過(guò)定制系統(tǒng)模型的調(diào)用模式，來(lái)實(shí)現(xiàn)對(duì)更多類型驅(qū)動(dòng)的支持；也可以通過(guò)定制更多的功能，例如，模擬用戶使用ifconfig查詢網(wǎng)絡(luò)參數(shù)的功能，來(lái)達(dá)到更高的代碼覆蓋率。這樣設(shè)計(jì)的好處是用戶可以通過(guò)定制系統(tǒng)模型來(lái)模擬特定場(chǎng)景和驅(qū)動(dòng)功能，使測(cè)試更加靈活和自由，體現(xiàn)了符號(hào)驅(qū)動(dòng)環(huán)境的可定制性。另外，系統(tǒng)模型的設(shè)計(jì)使得驅(qū)動(dòng)可以鏈接成一個(gè)目標(biāo)文件，從而在KLEE中進(jìn)行符號(hào)執(zhí)行分析。

3.2驅(qū)動(dòng)與內(nèi)核的交互

驅(qū)動(dòng)通過(guò)使用內(nèi)核提供的接口和結(jié)構(gòu)，來(lái)輔助完成驅(qū)動(dòng)自身的功能。例如使用kmalloc()函數(shù)來(lái)申請(qǐng)內(nèi)存等。符號(hào)驅(qū)動(dòng)環(huán)境中的內(nèi)核接口主要提供功能上的實(shí)現(xiàn)及相應(yīng)的檢測(cè)規(guī)則。驅(qū)動(dòng)中使用的內(nèi)核接口可能會(huì)失敗，一個(gè)魯棒的驅(qū)動(dòng)在這種情況下也不會(huì)簡(jiǎn)單地崩潰，而會(huì)嘗試恢復(fù)或者停止工作并報(bào)告問(wèn)題，符號(hào)驅(qū)動(dòng)環(huán)境對(duì)這種情況也進(jìn)行了模擬。本文設(shè)計(jì)了以下原則來(lái)實(shí)現(xiàn)內(nèi)核接口：成功時(shí)，簡(jiǎn)化地實(shí)現(xiàn)Linux系統(tǒng)中原函數(shù)的功能；失敗時(shí)，使用符號(hào)執(zhí)行返回相應(yīng)的失敗值；在需要的地方添加檢測(cè)規(guī)則來(lái)實(shí)現(xiàn)對(duì)漏洞的檢測(cè)。

為了檢測(cè)未進(jìn)行任何改動(dòng)的驅(qū)動(dòng)源碼中的漏洞，需要在符號(hào)驅(qū)動(dòng)環(huán)境的內(nèi)核接口中添加若干檢測(cè)規(guī)則。針對(duì)各種類型的漏洞，可以實(shí)現(xiàn)不同的檢測(cè)規(guī)則對(duì)其進(jìn)行檢測(cè)。以在spin_lock中實(shí)現(xiàn)的檢測(cè)規(guī)則為例：

voidspin_lock(spinlock_t *a) {

if(a→flags !=unlock) {

klee_warning("doublelock ");

klee_stace_trace();

}

a→flags=lock;

}

當(dāng)驅(qū)動(dòng)調(diào)用spin_lock函數(shù)時(shí)，通過(guò)修改的內(nèi)核結(jié)構(gòu)spin_lock_t中狀態(tài)變量來(lái)判斷鎖是否處于unlock狀態(tài)，如果鎖處于lock狀態(tài)則報(bào)錯(cuò)；如果鎖處于unlock狀態(tài)則將其標(biāo)記為lock狀態(tài)，以便下次檢測(cè)。spin_unlock中也會(huì)實(shí)現(xiàn)類似的規(guī)則。綜合這兩個(gè)函數(shù)中的規(guī)則可以檢測(cè)出驅(qū)動(dòng)中的doublelock和doublefree的漏洞。

這一設(shè)計(jì)原則的優(yōu)勢(shì)如下：簡(jiǎn)化實(shí)現(xiàn)內(nèi)核接口功能，可以減少在內(nèi)核中符號(hào)執(zhí)行的時(shí)間，使整個(gè)測(cè)試更加快速。通過(guò)分支路徑來(lái)模擬驅(qū)動(dòng)調(diào)用內(nèi)核接口失敗的可能性，可以模擬出驅(qū)動(dòng)在真實(shí)執(zhí)行時(shí)很少發(fā)生但是很可能出問(wèn)題的情況，提高了覆蓋率。在內(nèi)核接口中添加檢測(cè)規(guī)則，可以精確定位到漏洞發(fā)生的位置，解決了可觀測(cè)性的問(wèn)題，同時(shí)體現(xiàn)了符號(hào)驅(qū)動(dòng)環(huán)境的可擴(kuò)展性。

3.3驅(qū)動(dòng)與設(shè)備的交互

驅(qū)動(dòng)通過(guò)設(shè)備的交互來(lái)獲取設(shè)備的輸入和對(duì)設(shè)備進(jìn)行輸出，本文根據(jù)SymDrive的思想，設(shè)計(jì)并改進(jìn)了符號(hào)化設(shè)備來(lái)輔助完成這一交互，減少了不必要的符號(hào)值，改善了中斷處理函數(shù)調(diào)用的次數(shù)，以及采用符號(hào)值具體化的策略來(lái)解決路徑爆炸的部分問(wèn)題。下邊分三個(gè)部分進(jìn)行具體說(shuō)明。

3.3.1符號(hào)化I/O

驅(qū)動(dòng)中的I/O主要分為端口I/O和內(nèi)存映射I/O，其設(shè)計(jì)原則為：讀操作返回符號(hào)值；寫(xiě)操作忽略。讀操作返回符號(hào)值可以模擬設(shè)備出錯(cuò)的情況，檢測(cè)驅(qū)動(dòng)能否從異常狀態(tài)恢復(fù)，達(dá)到執(zhí)行的高覆蓋率。寫(xiě)操作忽略不會(huì)影響到驅(qū)動(dòng)的執(zhí)行。端口I/O和內(nèi)存映射I/O通過(guò)不同的策略來(lái)實(shí)現(xiàn)：端口I/O通過(guò)重寫(xiě)如inb的指令來(lái)實(shí)現(xiàn)；內(nèi)存映射I/O則標(biāo)記一段內(nèi)存空間，當(dāng)讀取這一范圍的值則返回符號(hào)值，向這一范圍寫(xiě)值則忽略。

SymDrive的內(nèi)存映射I/O的策略限于動(dòng)態(tài)執(zhí)行，是將整個(gè)映射的區(qū)域符號(hào)化。本文的內(nèi)存映射I/O策略與SymDrive相比，減少了符號(hào)值的數(shù)量，節(jié)約了約束求解器求解符號(hào)值的時(shí)間。

3.3.2符號(hào)化中斷

設(shè)備的一個(gè)特性是可以產(chǎn)生中斷，從而觸發(fā)中斷處理函數(shù)的運(yùn)行。本文在SymDrive策略的基礎(chǔ)上，設(shè)計(jì)了一種新的策略來(lái)實(shí)現(xiàn)中斷的觸發(fā)，加快了執(zhí)行速度。SymDrive實(shí)現(xiàn)的策略為：在每個(gè)驅(qū)動(dòng)和內(nèi)核轉(zhuǎn)換的地方觸發(fā)注冊(cè)的中斷；改進(jìn)的策略為：在系統(tǒng)模型中特定的時(shí)機(jī)觸發(fā)注冊(cè)的中斷。

前者在實(shí)用和簡(jiǎn)潔中取得了一個(gè)折衷，能夠保證中斷被充分地調(diào)用，使驅(qū)動(dòng)的檢測(cè)更加完備，但是會(huì)生成一些本不會(huì)發(fā)生的中斷。后者在一些特定驅(qū)動(dòng)中可以有很好的實(shí)用性，可以為系統(tǒng)模型中的定制驅(qū)動(dòng)功能提供支持，如網(wǎng)卡驅(qū)動(dòng)的中斷用于觸發(fā)收包，但存在漏掉驅(qū)動(dòng)的中斷處理中漏洞的可能性。

3.3.3符號(hào)化DMA

很多驅(qū)動(dòng)都使用DMA操作來(lái)與設(shè)備進(jìn)行數(shù)據(jù)交互，本文仿照內(nèi)存映射I/O設(shè)計(jì)了DMA的執(zhí)行策略：當(dāng)驅(qū)動(dòng)調(diào)用一個(gè)DMA映射函數(shù)時(shí)，會(huì)分配一段DMA緩沖并進(jìn)行標(biāo)記。每次對(duì)這一緩沖進(jìn)行讀操作時(shí)返回符號(hào)值，所有寫(xiě)操作被忽略；當(dāng)驅(qū)動(dòng)取消DMA映射時(shí)，將這段緩沖的標(biāo)記取消，并恢復(fù)成之前的狀態(tài)。

和I/O相比，DMA更多地用于大規(guī)模數(shù)據(jù)的交互，所以更可能發(fā)生路徑爆炸的問(wèn)題。例如，網(wǎng)卡驅(qū)動(dòng)的收包過(guò)程依賴于DMA映射，如果返回符號(hào)值會(huì)導(dǎo)致收包循環(huán)無(wú)法結(jié)束。針對(duì)這種情況，本文參照硬件規(guī)范將一部分符號(hào)值具體化(就上例來(lái)說(shuō)為指定收包的數(shù)目)，來(lái)解決可能發(fā)生的路徑爆炸問(wèn)題。

4實(shí)驗(yàn)結(jié)果及分析

檢測(cè)環(huán)境配置如下：24核Intel2.40GHz，E5645CPU，內(nèi)存12GB。操作系統(tǒng)為Ubuntu12.04LTS，相關(guān)軟件版本為L(zhǎng)LVM2.9版本，KLEE2013.12.11版本。在符號(hào)驅(qū)動(dòng)環(huán)境下執(zhí)行Linux內(nèi)核3.12版本中的lp打印機(jī)驅(qū)動(dòng)和e100網(wǎng)卡驅(qū)動(dòng)，結(jié)果如表2所示。

Table 2　 Detecting results of Linux drivers

從表2中可以看出，符號(hào)驅(qū)動(dòng)環(huán)境檢測(cè)出lp打印機(jī)驅(qū)動(dòng)中一個(gè)整數(shù)溢出漏洞，以及e100網(wǎng)卡驅(qū)動(dòng)中的一個(gè)DMA映射相關(guān)漏洞。這一結(jié)果證明了符號(hào)執(zhí)行環(huán)境的可行性。

與SymDrive動(dòng)態(tài)符號(hào)分析工具進(jìn)行性能對(duì)比如表3所示。

Table 3　 Performance comparison between symbolic

從表3的結(jié)果可以看到：符號(hào)驅(qū)動(dòng)環(huán)境的檢測(cè)時(shí)間比SymDrive快90%以上；符號(hào)驅(qū)動(dòng)環(huán)境的函數(shù)覆蓋率比SymDrive高20%左右。

從時(shí)間角度來(lái)說(shuō)，SymDrive在虛擬機(jī)上運(yùn)行真實(shí)的Linux系統(tǒng)，所以會(huì)在內(nèi)核的執(zhí)行中耗費(fèi)大量時(shí)間；而符號(hào)執(zhí)行環(huán)境實(shí)現(xiàn)了簡(jiǎn)化的內(nèi)核接口，因此運(yùn)行時(shí)間主要集中在驅(qū)動(dòng)內(nèi)部，所以執(zhí)行的指令數(shù)更少，運(yùn)行時(shí)間更短。從函數(shù)覆蓋比角度來(lái)說(shuō)，由于SymDrive在初始化驅(qū)動(dòng)時(shí)采用了成功路徑優(yōu)先的調(diào)度策略，而符號(hào)驅(qū)動(dòng)環(huán)境覆蓋了可能發(fā)生失敗的路徑，所以覆蓋率更高。這一結(jié)果也表明符號(hào)驅(qū)動(dòng)環(huán)境基本達(dá)到了設(shè)計(jì)的目的：快速檢測(cè)以及高覆蓋率。

5結(jié)束語(yǔ)

本文提出并實(shí)現(xiàn)了符號(hào)驅(qū)動(dòng)環(huán)境這一輔助檢測(cè)Linux驅(qū)動(dòng)中漏洞的工具，結(jié)合了靜態(tài)分析、符號(hào)執(zhí)行和動(dòng)態(tài)分析工具的特點(diǎn)，改善了驅(qū)動(dòng)檢測(cè)中面臨的觀測(cè)性和覆蓋率的問(wèn)題。在符號(hào)驅(qū)動(dòng)環(huán)境中，用戶可以通過(guò)定制系統(tǒng)模型來(lái)支持更多的驅(qū)動(dòng)，以及實(shí)現(xiàn)特定的功能，還可以通過(guò)添加規(guī)則來(lái)實(shí)現(xiàn)針對(duì)各種類型漏洞的檢測(cè)。實(shí)驗(yàn)中以lp打印機(jī)驅(qū)動(dòng)和e100網(wǎng)卡驅(qū)動(dòng)為例，成功使用該工具檢測(cè)出兩個(gè)真實(shí)的漏洞，表明其可行性；通過(guò)與SymDrive的性能比較，表明了符號(hào)驅(qū)動(dòng)環(huán)境有快速和覆蓋率高的優(yōu)勢(shì)。

符號(hào)驅(qū)動(dòng)環(huán)境還需要進(jìn)一步改進(jìn)和完善，今后可以在以下幾個(gè)方面進(jìn)行更深一步的研究：(1)對(duì)競(jìng)爭(zhēng)、調(diào)度引起的線程或進(jìn)程間漏洞的檢測(cè)；(2)優(yōu)化調(diào)度策略和路徑剪枝策略，進(jìn)一步解決路徑爆炸問(wèn)題；(3)支持更多類型的驅(qū)動(dòng)，添加更多的檢測(cè)規(guī)則。

參考文獻(xiàn):

[1]ChouA,YangJ,ChelfB,etal.Anempiricalstudyofoperatingsystemserrors[C]//Procofthe8thACMSymposiumonOperatingSystemPrinciples, 2001:73-88.

[2]SwiftMM,MartinS,LevyHM,etal.Nooks:Anarchitectureforreliabledevicedrivers[C]//Procofthe10thWorkshoponACMSIGOPSEuropeanWorkshop, 2002:102-107.

[3]WangX,ChenH,JiaZ,etal.ImprovingintegersecurityforsystemswithKINT[C]//Procofthe10thUSENIXConferenceonOperatingSystemsDesignandImplementation, 2012:163-177.

[4]BeyerD,HenzingerTA,JhalaR,etal.ThesoftwaremodelcheckerBLAST:Applicationstosoftwareengineering[J].InternationalJournalonSoftwareToolsforTechnologyTransfer, 2007,9(5-6):505-525.

[5]BallT,BounimovaE,CookB,etal.Throughstaticanalysisofdevicedrivers[J].ACMSIGOPSOperatingSystemsRe-

view, 2006, 40(4):73-85.

[6]ChipounovV,KuznetsovV,CandeaG.S2E:Aplatformforin-vivomulti-pathanalysisofsoftwaresystems[J].ACMSIGARCHComputerArchitectureNews, 2011, 39(1):265-278.

[7]CadarC,DunbarD,EnglerDR.KLEE:Unassistedandautomaticgenerationofhigh-coveragetestsforcomplexsystemsprograms[C]//ProcofOSDI, 2008:209-224.

[8]LattnerC,AdveV.LLVM:Acompilationframeworkforlifelongprogramanalysis&transformation[C]//ProcofInternationalSymposiumonCodeGenerationandOptimization, 2004:75-86.

[9]KuznetsovV,ChipounovV,CandeaG.Testingclosed-sourcebinarydevicedriverswithDDT[C]//Procofthe2010USENIXAnnualTechnicalConference, 2010.

[10]RenzelmannMJ,KadavA,SwiftMM.Symdrive:Testingdriverswithoutdevices[C]//ProcofOSDI,2012:4.

[11]NeculaGC,McPeakS,RahulSP,etal.CIL:IntermediatelanguageandtoolsforanalysisandtransformationofCprograms[C]//ProcofCompilerConstruction, 2002:213-228.

范文良(1988-),男,吉林九臺(tái)人，碩士生，研究方向?yàn)椴僮飨到y(tǒng)和計(jì)算機(jī)信息安全。E-mail:fanwlexca@gmail.com

FANWen-liang,bornin1988,MScandidate,hisresearchinterestsincludeoperatingsystem,andcomputerinformationsecurity.