輔助檢測Linux驅動中漏洞的符號驅動環境

輔助檢測Linux驅動中漏洞的符號驅動環境*

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

(清華大學計算機科學與技術系，北京 100084)

摘要：Linux系統中的驅動漏洞被證實是內核漏洞的主要來源，可以被利用導致嚴重的安全問題。通過系統模型、驅動與內核的交互和驅動與設備的交互這三部分的設計與實現，構建了符號驅動環境，用于輔助檢測Linux驅動中的漏洞。使用符號驅動環境對兩個真實的驅動進行檢測，成功檢測出了兩個漏洞，證實了該工具的可行性。與SymDrive工具的性能相比，符號驅動環境執行速度快90%，覆蓋率提高20%。

關鍵詞：驅動漏洞；漏洞檢測；符號執行；驅動環境

中圖分類號：TP309.2 文獻標志碼：A

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

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

基金項目：國家自然科學基金資助項目(61170050)；核高基重大專項基金資助項目(2012ZX01039-004)

作者簡介:

通信地址：100084 北京市清華大學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是一個使用廣泛的開源操作系統，由于每個用戶都可以獲得并分析Linux的源代碼，再加上近年來Android系統(基于Linux)在移動端廣泛使用，使得Linux系統的安全性面臨著重大的挑戰。近來很多研究表明，內核驅動程序(簡稱驅動)是內核漏洞的主要制造者。斯坦福大學的一項研究表明[1]，Linux驅動中的漏洞要比內核中的其余部分多3～7倍。在另一流行的操作系統Windows中，也有研究表明[2]，有27%的系統崩潰是由驅動所引起的，相比之下由內核本身引起的只有2%。這些都證明了安全驅動的重要性。

驅動中的漏洞類型有硬件依賴錯誤、API誤用、競爭、申請釋放不匹配、內存泄露、驅動接口誤用、指針問題等。現有的漏洞檢測工具主要分為：靜態分析工具、符號執行工具和動態分析工具。使用現有的工具檢測驅動中的漏洞存在以下問題：

(1)觀測性：驅動誤用內核接口的真正位置很難檢測，這是由于大多數驅動對內核接口的誤用不會立即導致系統崩潰，而是使系統處于不穩定的狀態，在之后引發崩潰或異常行為。

(2)覆蓋率：驅動中的漏洞通常會發生在一些很少見的狀態中，傳統的測試工具通常無法覆蓋到這些狀態，也就無法檢測出這些漏洞。

針對上述問題，本文首先介紹了用于漏洞檢測的三種主要方法：靜態分析、符號執行和動態分析。然后，綜合上述方法的特點，提出了輔助檢測Linux驅動中漏洞的原型系統——符號驅動環境，改進了靜態分析誤報率高，動態分析依賴輸入、難以定位漏洞位置、符號執行會引起路徑爆炸的問題。最后，通過將符號驅動環境應用于Linux中的lp打印機驅動和e100網卡驅動，檢測出兩個真實存在的漏洞，驗證了該原型系統的可行性，并通過與SymDrive的對比，表明了符號驅動環境執行速度更快，覆蓋率更高。

2相關工作

2.1靜態分析

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

SDV具有典型的代表性，其主要包括Windows系統的模型及驅動運行的模擬環境以及60余條內核接口的使用規則。SDV在系統模型中模擬運行驅動源碼，在內核接口中通過規則檢測對其的正確使用，最后輸出錯誤報告。SDV通過檢測規則來定義內核接口的正確使用，從而解決了驅動檢測中觀測性的問題。

微軟公司使用SDV對大量驅動進行了檢測并發現了120余個嚴重的漏洞，但SDV仍存在如下問題：首先，SDV是一個閉源工具，無法將其移植用于檢測Linux驅動中漏洞；其次，SDV限于靜態分析，難以分析函數指針以及用于內存檢測等；最后，SDV雖能夠覆蓋到驅動調用內核接口失敗的情況，但是對驅動中由于設備輸入而引起的分支情況覆蓋率很低。

2.2符號執行

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

Figure 1　Example of symbolic execution 圖1　符號執行例子

設x為符號值，在遇到x<5這一分支判斷時，執行引擎會分支并形成兩條路徑，一條路徑關于x的約束表達式是x<5，該路徑繼續執行判斷體內的語句；另一條路徑關于x的約束表達式是x≥5，該路徑跳過判斷體繼續執行。判斷體中的x<0同理。設sysFn函數中要輸出x的值，求解器就會在x<5這一范圍內給x賦隨機值，比如0。

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

2.3動態分析

動態分析是指在運行時監控程序行為、收集程序信息進行漏洞檢測，一般通過構造特定的輸入來觸發漏洞。動態分析可以解決靜態分析很難解決的問題，如指針、內存檢測等，但動態分析需要很大的工作量來構造輸入，由于觀測性的問題，動態分析也很難定位驅動中漏洞的位置。動態分析往往和別的分析方法綜合使用，檢測效果較好的工具有：洛桑理工學院基于S2E開發的DDT[9]，用于檢測Windows網卡驅動中的漏洞；威斯康辛大學基于S2E開發的SymDrive[10]，用于檢測Linux驅動中的多種漏洞。

SymDrive的總體結構見圖2。SymDrive是源碼級的工具，首先使用源碼轉換工具CIL[11]對驅動源碼進行插樁，來輔助動態符號執行，然后使用符號化設備來模擬硬件產生的輸入，最后將驅動運行在QEMU虛擬機中執行檢測。SymDrive提出并實現了符號化設備這一思想，其原理如下：首先，虛擬機可以發現并配置虛擬的符號化設備，然后加載合適的驅動；其次，當驅動需要設備提供輸入時，符號化設備可以產生一系列符號值，來輔助驅動的符號執行，達到高覆蓋率測試的目的。SymDrive的檢測依賴CIL的源碼插樁，通過在驅動的源代碼中插入一些相應的規則，在動態執行到該檢測點時驗證當前路徑能否通過該檢測。這種檢測方式比較準確，但由于其真實地執行代碼，會花費大量的時間在內核執行上，所以執行時間通常很長；另外，由于符號化設備會產生大量的符號值，經常會造成路徑爆炸，SymDrive提供了注釋插件來規避這一問題。

Figure 2　Architecture of SymDrive 圖2　SymDrive總體結構

3符號驅動環境

本文在SymDrive的符號化設備和KLEE符號執行的基礎上，實現了符號驅動環境——輔助檢測Linux驅動中漏洞的工具。符號驅動環境使用符號執行改進了SDV覆蓋率低的問題，使用Linux系統模型解決了無法在KLEE中執行驅動的問題，使用內核接口和改進的符號化設備改進了SymDrive執行時間長和路徑爆炸的問題。在符號驅動環境上可以通過定制系統行為來模擬驅動功能、支持不同類型驅動，以及添加檢測規則來檢測多種類型的漏洞。符號驅動環境的設計目的是為Linux驅動提供一個輕量級的運行環境，更充分地測試驅動代碼，減少內核代碼的執行時間，從而減少測試時間，提高代碼覆蓋率。

符號驅動環境具備以下特點：

(1)可定制性：不同類型的驅動的功能各不相同，如網卡驅動可用于發包、收包、查詢網絡參數，LED驅動可用于控制LED燈的亮、暗等。符號驅動環境通過系統模型管理操作系統主動調用驅動的流程，用戶可以簡單地通過定制系統模型來模擬驅動的功能，實現對不同類型驅動的支持，提高對驅動代碼測試的覆蓋率。

(2)可擴展性：符號驅動環境通過規則來檢測漏洞，不同類型的漏洞需要有不同的檢測規則，本文在符號驅動環境中添加了常見的如內存、鎖等方面的檢測規則。符號驅動環境還可以添加更多的檢測規則，從而實現對更多類型漏洞的檢測，提高了整個工具的擴展性。

符號驅動環境的結構如圖3所示。符號驅動環境主要分為系統模型、驅動與內核的交互以及驅動與設備的交互三部分，其執行流程如下：首先，通過系統模型來主動調用驅動；然后，當驅動執行到內核接口時，通過簡化的內核實現來完成相應的功能并執行檢測；之后，當驅動需要與設備交互時，通過符號化設備來完成交互；最后，完成系統模型的調用邏輯之后，輸出錯誤報告并使用求解器求解出可以觸發漏洞的相關輸入的具體值。

Figure 3　Architecture of symboilc driver environment 圖3　符號驅動環境總體結構

3.1系統模型

系統模型用于模擬Linux系統對驅動調用的流程和完成驅動功能(如觸發網卡驅動收包)，以達到可定制地執行各種類型驅動的目的。每一種類型的驅動都有其固定的調用模式，這一模式也反映在每類驅動都有一些固定的函數指針上，如表1所示(以e100網卡驅動為例)。

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

下邊以e100網卡驅動為例，說明定制了收、發包功能的系統模型的調用模式：首先，通過module_init()暴露的驅動函數開啟驅動的注冊，并調用probe和open函數指針完成驅動的注冊；然后，調用ndo_start_xmit函數指針模擬實現發包的功能，模擬硬中斷觸發收包，調用驅動注冊的中斷處理函數完成收包的操作；最后，以與注冊相反的順序，調用close、remove函數指針和module_exit()暴露的函數來注銷驅動。

以上就是定制了收、發包功能的網卡驅動的調用模式，這一調用模式能覆蓋50%左右的網卡驅動函數，包括注冊中讀取設備配置信息等函數，發包、收包的主要函數，以及注銷中釋放內存、垃圾回收等函數。用戶可以通過定制系統模型的調用模式，來實現對更多類型驅動的支持；也可以通過定制更多的功能，例如，模擬用戶使用ifconfig查詢網絡參數的功能，來達到更高的代碼覆蓋率。這樣設計的好處是用戶可以通過定制系統模型來模擬特定場景和驅動功能，使測試更加靈活和自由，體現了符號驅動環境的可定制性。另外，系統模型的設計使得驅動可以鏈接成一個目標文件，從而在KLEE中進行符號執行分析。

3.2驅動與內核的交互

驅動通過使用內核提供的接口和結構，來輔助完成驅動自身的功能。例如使用kmalloc()函數來申請內存等。符號驅動環境中的內核接口主要提供功能上的實現及相應的檢測規則。驅動中使用的內核接口可能會失敗，一個魯棒的驅動在這種情況下也不會簡單地崩潰，而會嘗試恢復或者停止工作并報告問題，符號驅動環境對這種情況也進行了模擬。本文設計了以下原則來實現內核接口：成功時，簡化地實現Linux系統中原函數的功能；失敗時，使用符號執行返回相應的失敗值；在需要的地方添加檢測規則來實現對漏洞的檢測。

為了檢測未進行任何改動的驅動源碼中的漏洞，需要在符號驅動環境的內核接口中添加若干檢測規則。針對各種類型的漏洞，可以實現不同的檢測規則對其進行檢測。以在spin_lock中實現的檢測規則為例：

voidspin_lock(spinlock_t *a) {

if(a→flags !=unlock) {

klee_warning("doublelock ");

klee_stace_trace();

}

a→flags=lock;

}

當驅動調用spin_lock函數時，通過修改的內核結構spin_lock_t中狀態變量來判斷鎖是否處于unlock狀態，如果鎖處于lock狀態則報錯；如果鎖處于unlock狀態則將其標記為lock狀態，以便下次檢測。spin_unlock中也會實現類似的規則。綜合這兩個函數中的規則可以檢測出驅動中的doublelock和doublefree的漏洞。

這一設計原則的優勢如下：簡化實現內核接口功能，可以減少在內核中符號執行的時間，使整個測試更加快速。通過分支路徑來模擬驅動調用內核接口失敗的可能性，可以模擬出驅動在真實執行時很少發生但是很可能出問題的情況，提高了覆蓋率。在內核接口中添加檢測規則，可以精確定位到漏洞發生的位置，解決了可觀測性的問題，同時體現了符號驅動環境的可擴展性。

3.3驅動與設備的交互

驅動通過設備的交互來獲取設備的輸入和對設備進行輸出，本文根據SymDrive的思想，設計并改進了符號化設備來輔助完成這一交互，減少了不必要的符號值，改善了中斷處理函數調用的次數，以及采用符號值具體化的策略來解決路徑爆炸的部分問題。下邊分三個部分進行具體說明。

3.3.1符號化I/O

驅動中的I/O主要分為端口I/O和內存映射I/O，其設計原則為：讀操作返回符號值；寫操作忽略。讀操作返回符號值可以模擬設備出錯的情況，檢測驅動能否從異常狀態恢復，達到執行的高覆蓋率。寫操作忽略不會影響到驅動的執行。端口I/O和內存映射I/O通過不同的策略來實現：端口I/O通過重寫如inb的指令來實現；內存映射I/O則標記一段內存空間，當讀取這一范圍的值則返回符號值，向這一范圍寫值則忽略。

SymDrive的內存映射I/O的策略限于動態執行，是將整個映射的區域符號化。本文的內存映射I/O策略與SymDrive相比，減少了符號值的數量，節約了約束求解器求解符號值的時間。

3.3.2符號化中斷

設備的一個特性是可以產生中斷，從而觸發中斷處理函數的運行。本文在SymDrive策略的基礎上，設計了一種新的策略來實現中斷的觸發，加快了執行速度。SymDrive實現的策略為：在每個驅動和內核轉換的地方觸發注冊的中斷；改進的策略為：在系統模型中特定的時機觸發注冊的中斷。

前者在實用和簡潔中取得了一個折衷，能夠保證中斷被充分地調用，使驅動的檢測更加完備，但是會生成一些本不會發生的中斷。后者在一些特定驅動中可以有很好的實用性，可以為系統模型中的定制驅動功能提供支持，如網卡驅動的中斷用于觸發收包，但存在漏掉驅動的中斷處理中漏洞的可能性。

3.3.3符號化DMA

很多驅動都使用DMA操作來與設備進行數據交互，本文仿照內存映射I/O設計了DMA的執行策略：當驅動調用一個DMA映射函數時，會分配一段DMA緩沖并進行標記。每次對這一緩沖進行讀操作時返回符號值，所有寫操作被忽略；當驅動取消DMA映射時，將這段緩沖的標記取消，并恢復成之前的狀態。

和I/O相比，DMA更多地用于大規模數據的交互，所以更可能發生路徑爆炸的問題。例如，網卡驅動的收包過程依賴于DMA映射，如果返回符號值會導致收包循環無法結束。針對這種情況，本文參照硬件規范將一部分符號值具體化(就上例來說為指定收包的數目)，來解決可能發生的路徑爆炸問題。

4實驗結果及分析

檢測環境配置如下：24核Intel2.40GHz，E5645CPU，內存12GB。操作系統為Ubuntu12.04LTS，相關軟件版本為LLVM2.9版本，KLEE2013.12.11版本。在符號驅動環境下執行Linux內核3.12版本中的lp打印機驅動和e100網卡驅動，結果如表2所示。

Table 2　 Detecting results of Linux drivers

從表2中可以看出，符號驅動環境檢測出lp打印機驅動中一個整數溢出漏洞，以及e100網卡驅動中的一個DMA映射相關漏洞。這一結果證明了符號執行環境的可行性。

與SymDrive動態符號分析工具進行性能對比如表3所示。

Table 3　 Performance comparison between symbolic

從表3的結果可以看到：符號驅動環境的檢測時間比SymDrive快90%以上；符號驅動環境的函數覆蓋率比SymDrive高20%左右。

從時間角度來說，SymDrive在虛擬機上運行真實的Linux系統，所以會在內核的執行中耗費大量時間；而符號執行環境實現了簡化的內核接口，因此運行時間主要集中在驅動內部，所以執行的指令數更少，運行時間更短。從函數覆蓋比角度來說，由于SymDrive在初始化驅動時采用了成功路徑優先的調度策略，而符號驅動環境覆蓋了可能發生失敗的路徑，所以覆蓋率更高。這一結果也表明符號驅動環境基本達到了設計的目的：快速檢測以及高覆蓋率。

5結束語

本文提出并實現了符號驅動環境這一輔助檢測Linux驅動中漏洞的工具，結合了靜態分析、符號執行和動態分析工具的特點，改善了驅動檢測中面臨的觀測性和覆蓋率的問題。在符號驅動環境中，用戶可以通過定制系統模型來支持更多的驅動，以及實現特定的功能，還可以通過添加規則來實現針對各種類型漏洞的檢測。實驗中以lp打印機驅動和e100網卡驅動為例，成功使用該工具檢測出兩個真實的漏洞，表明其可行性；通過與SymDrive的性能比較，表明了符號驅動環境有快速和覆蓋率高的優勢。

符號驅動環境還需要進一步改進和完善，今后可以在以下幾個方面進行更深一步的研究：(1)對競爭、調度引起的線程或進程間漏洞的檢測；(2)優化調度策略和路徑剪枝策略，進一步解決路徑爆炸問題；(3)支持更多類型的驅動，添加更多的檢測規則。

參考文獻:

[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-),男,吉林九臺人，碩士生，研究方向為操作系統和計算機信息安全。E-mail:fanwlexca@gmail.com

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