賀 灝，夏群峰，甘水滔

(江南計(jì)算技術(shù)研究所，江蘇無(wú)錫214000)

基于規(guī)則檢查的網(wǎng)卡驅(qū)動(dòng)程序脆弱性研究

賀 灝，夏群峰，甘水滔

(江南計(jì)算技術(shù)研究所，江蘇無(wú)錫214000)

在計(jì)算機(jī)系統(tǒng)中，驅(qū)動(dòng)程序相當(dāng)于操作系統(tǒng)和底層硬件的交互紐帶，其正確性不容忽視。以Linux內(nèi)核網(wǎng)卡驅(qū)動(dòng)程序?yàn)橹饕治鰧?duì)象，通過(guò)對(duì)網(wǎng)卡驅(qū)動(dòng)程序的基本功能模塊進(jìn)行分析，借助符號(hào)執(zhí)行技術(shù)，提出了一種基于規(guī)則檢查的網(wǎng)卡驅(qū)動(dòng)程序分析方法，構(gòu)建了一個(gè)自動(dòng)化分析系統(tǒng)。針對(duì)Linux 2.6.29版本的內(nèi)核，利用該系統(tǒng)進(jìn)行測(cè)試，結(jié)果表明該系統(tǒng)可以快速有效發(fā)現(xiàn)新脆弱性。

網(wǎng)卡驅(qū)動(dòng)；脆弱性；符號(hào)執(zhí)行；規(guī)則檢查

0 引言

隨著計(jì)算機(jī)在人類(lèi)生活中的快速普及，在一些特殊的應(yīng)用領(lǐng)域中，比如金融、交通、工業(yè)等領(lǐng)域，對(duì)計(jì)算機(jī)系統(tǒng)的安全性要求極高，在這些領(lǐng)域里，各種各樣的極其重視安全性的系統(tǒng)除了依賴(lài)外部的定制硬件外，還需要依靠總線與計(jì)算機(jī)系統(tǒng)內(nèi)部進(jìn)行通信。因此，總線設(shè)備驅(qū)動(dòng)程序、網(wǎng)絡(luò)設(shè)備驅(qū)動(dòng)程序、塊存儲(chǔ)設(shè)備驅(qū)動(dòng)程序等在計(jì)算機(jī)系統(tǒng)中非常常見(jiàn)。

對(duì)于驅(qū)動(dòng)程序的脆弱性分析非常必要，無(wú)論是Kernel中已經(jīng)集成的驅(qū)動(dòng)程序模塊，還是第三方硬件生產(chǎn)商開(kāi)發(fā)的設(shè)備驅(qū)動(dòng)程序，其代碼都非常復(fù)雜，涉及到操作系統(tǒng)和具體的硬件設(shè)備兩部分的代碼，在結(jié)構(gòu)上這兩部分的代碼也沒(méi)有明確清晰的條理性，對(duì)于第三方引入的設(shè)備驅(qū)動(dòng)程序，通常硬件生產(chǎn)商對(duì)其測(cè)試也并不充分。但驅(qū)動(dòng)程序具有非常高的權(quán)限，而且也基本在內(nèi)核態(tài)中運(yùn)行，一旦驅(qū)動(dòng)程序因?yàn)榇嗳跣援a(chǎn)生了崩潰或異常，對(duì)于系統(tǒng)的危害將是致命的，因此需要對(duì)驅(qū)動(dòng)程序進(jìn)行脆弱性分析。

1 內(nèi)核驅(qū)動(dòng)脆弱性

驅(qū)動(dòng)程序在Kernel中是極其重要的部分，Linux系統(tǒng)的內(nèi)核驅(qū)動(dòng)程序以?xún)?nèi)核模塊的形式被集成在系統(tǒng)中。由圖1可以看出，內(nèi)核驅(qū)動(dòng)程序的代碼量增長(zhǎng)速度遠(yuǎn)遠(yuǎn)快于其它模塊的代碼量，其增長(zhǎng)趨勢(shì)也接近于內(nèi)核的代碼量。

圖1 Linux Kernel代碼增長(zhǎng)圖(單位:百萬(wàn))

斯坦福大學(xué)(Stanford University)曾經(jīng)有一份針對(duì)內(nèi)核驅(qū)動(dòng)程序脆弱性數(shù)量占比的研究[1]，其結(jié)果如圖2所示。

圖2 操作系統(tǒng)中錯(cuò)誤在模塊中的分布

該研究結(jié)果顯示，在整個(gè)Linux系統(tǒng)中，內(nèi)核驅(qū)動(dòng)程序出現(xiàn)脆弱性的頻率遠(yuǎn)遠(yuǎn)高于其它內(nèi)核模塊，總體出現(xiàn)脆弱性的可能性是其它內(nèi)核模塊的3～7倍。

內(nèi)核驅(qū)動(dòng)程序存在大量異步事件，例如對(duì)于網(wǎng)卡驅(qū)動(dòng)程序而言，在出現(xiàn)新的數(shù)據(jù)包需要進(jìn)行發(fā)送的情況時(shí)，驅(qū)動(dòng)會(huì)控制DMA通道進(jìn)行數(shù)據(jù)的傳輸，但在實(shí)際操作中，驅(qū)動(dòng)程序?qū)用娴暮瘮?shù)調(diào)用結(jié)束卻并不一定說(shuō)明硬件設(shè)備完成了數(shù)據(jù)的發(fā)送。

當(dāng)Kernel對(duì)一個(gè)數(shù)據(jù)包A進(jìn)行發(fā)送后，ndo＿start＿xmit函數(shù)在完成功能后返回，緊接著Kernel又要發(fā)送數(shù)據(jù)包B，此時(shí)Kernel會(huì)再次調(diào)用ndo＿start＿xmit函數(shù)，而當(dāng)函數(shù)被調(diào)用時(shí)，之前傳送到網(wǎng)卡內(nèi)存的數(shù)據(jù)包A也許還未發(fā)送完畢，也就是說(shuō)，軟件層面的函數(shù)調(diào)用和具體的硬件設(shè)備執(zhí)行的行為是異步的。之所以產(chǎn)生這樣的問(wèn)題，是因?yàn)镵ernel中的高層次的代碼可以向網(wǎng)卡設(shè)備快速傳遞大量的數(shù)據(jù)包，而網(wǎng)卡設(shè)備的實(shí)際發(fā)送速度無(wú)法匹配內(nèi)存中接收數(shù)據(jù)包的速度。

因此在內(nèi)核驅(qū)動(dòng)程序運(yùn)行時(shí)，頻繁的中斷等操作使得代碼之間會(huì)出現(xiàn)大量的交錯(cuò)執(zhí)行，這也會(huì)使得動(dòng)態(tài)分析工具無(wú)法達(dá)到更高的代碼覆蓋率，并且即便發(fā)現(xiàn)了內(nèi)核驅(qū)動(dòng)程序的脆弱性，也很難對(duì)其進(jìn)行準(zhǔn)確的重現(xiàn)。

2 目標(biāo)分析

2.1 網(wǎng)卡驅(qū)動(dòng)

網(wǎng)絡(luò)設(shè)備，是Linux操作系統(tǒng)下三大標(biāo)準(zhǔn)設(shè)備類(lèi)型之一，主要為了完成高層網(wǎng)絡(luò)協(xié)議的底層數(shù)據(jù)傳輸和設(shè)備控制等功能。作為基本的PCI設(shè)備，網(wǎng)卡也要遵循相應(yīng)的PCI設(shè)備規(guī)范，即需要由總線編號(hào)、設(shè)備編號(hào)、功能編號(hào)來(lái)標(biāo)識(shí)網(wǎng)卡。

網(wǎng)卡有兩種內(nèi)部空間，其一是配置空間，需要借助BIOS功能才能實(shí)現(xiàn)訪問(wèn)，CPU不能直接訪問(wèn)該空間，其二是控制寄存器空間，經(jīng)過(guò)映射后，CPU可以直接進(jìn)行該空間的訪問(wèn)與控制。

在計(jì)算機(jī)設(shè)備通電后，所有硬件加電進(jìn)行初始化，此時(shí)BIOS會(huì)對(duì)所有PCI設(shè)備進(jìn)行檢查，并給設(shè)備分配不同的物理地址，當(dāng)OS初始化時(shí)，系統(tǒng)會(huì)給PCI設(shè)備分配pci＿dev結(jié)構(gòu)。內(nèi)核驅(qū)動(dòng)程序通過(guò)讀取 pci＿resource＿start()函數(shù)和 pci＿resource＿end()函數(shù)獲得寄存器空間地址，再利用ioremap()函數(shù)將該段位置映射到計(jì)算機(jī)主存中，這樣CPU就可以通過(guò)訪問(wèn)這段映射后的虛擬地址來(lái)實(shí)現(xiàn)對(duì)網(wǎng)卡硬件設(shè)備的訪問(wèn)和控制。

網(wǎng)卡的實(shí)際網(wǎng)絡(luò)傳輸功能，由net＿device結(jié)構(gòu)體現(xiàn)，該結(jié)構(gòu)存儲(chǔ)網(wǎng)卡的所有信息，數(shù)據(jù)結(jié)構(gòu)龐大。net＿device結(jié)構(gòu)由內(nèi)核驅(qū)動(dòng)程序初始化，其為上一層的協(xié)議提供了接口，是對(duì)特定適配器的抽象，該結(jié)構(gòu)體表示了絕大部分和硬件有關(guān)的屬性，而內(nèi)核驅(qū)動(dòng)程序則是在特定適配器的基礎(chǔ)上實(shí)現(xiàn)了該抽象。所以操作系統(tǒng)kernel對(duì)網(wǎng)卡的所有操作，本質(zhì)是對(duì)net＿device結(jié)構(gòu)操作，在此之外，其它對(duì)網(wǎng)卡的具體操作則是對(duì)adapter結(jié)構(gòu)體進(jìn)行操作。某種程度上，adapter結(jié)構(gòu)體體現(xiàn)了 net＿device結(jié)構(gòu)和 pci＿dev結(jié)構(gòu)的關(guān)聯(lián)性，也使得網(wǎng)卡驅(qū)動(dòng)程序?qū)崿F(xiàn)了與具體硬件設(shè)備適配器的無(wú)關(guān)性。

作為一個(gè)典型的PCI設(shè)備，網(wǎng)卡驅(qū)動(dòng)程序也應(yīng)由pci＿driver結(jié)構(gòu)體表示，也就是該結(jié)構(gòu)體的一個(gè)實(shí)例，驅(qū)動(dòng)程序在其中定義網(wǎng)卡相關(guān)的技術(shù)參數(shù)和相應(yīng)的操作函數(shù)，三個(gè)數(shù)據(jù)結(jié)構(gòu)之間的關(guān)系如圖3所示。

圖3 網(wǎng)卡驅(qū)動(dòng)程序數(shù)據(jù)結(jié)構(gòu)

2.2 規(guī)則分析

網(wǎng)卡設(shè)備屬于功能較為單一的PCI設(shè)備，系統(tǒng)對(duì)其的調(diào)用可以歸納為以下幾個(gè)步驟。

(1)分配并初始化新的net＿device對(duì)象；

(2)通過(guò)內(nèi)核提供的register＿netdev函數(shù)完成對(duì)驅(qū)動(dòng)的注冊(cè)；

(3)利用ifconfig調(diào)用ndo＿open函數(shù)打開(kāi)網(wǎng)卡接口；

(4)對(duì)于數(shù)據(jù)包的發(fā)送，處理較為簡(jiǎn)單。利用net＿device＿ops中的ndo＿start＿xmit函數(shù)進(jìn)行數(shù)據(jù)包的發(fā)送；

(5)對(duì)于數(shù)據(jù)包的接收，過(guò)程較為復(fù)雜，對(duì)于網(wǎng)卡驅(qū)動(dòng)程序，數(shù)據(jù)包何時(shí)到達(dá)是不確定的，因此當(dāng)需要接收數(shù)據(jù)包時(shí)，通常利用中斷的方式，當(dāng)接收到中斷指令時(shí)，系統(tǒng)才會(huì)完成數(shù)據(jù)包接收操作；

(6)利用ifconfig調(diào)用ndo＿stop函數(shù)關(guān)閉網(wǎng)卡接口；

(7)通過(guò)內(nèi)核提供的free＿netdev函數(shù)注銷(xiāo)。

針對(duì)網(wǎng)卡設(shè)備中系統(tǒng)對(duì)驅(qū)動(dòng)的調(diào)用關(guān)系，可以總結(jié)出網(wǎng)卡驅(qū)動(dòng)程序的工作流程圖如圖4所示。

圖4 網(wǎng)卡驅(qū)動(dòng)程序工作流程

依據(jù)調(diào)用關(guān)系，本文總結(jié)了網(wǎng)卡驅(qū)動(dòng)程序的調(diào)用模式函數(shù)功能表，以供規(guī)則檢測(cè)時(shí)使用。表1為benet驅(qū)動(dòng)的函數(shù)功能。

表1 網(wǎng)卡驅(qū)動(dòng)函數(shù)功能

3 插樁實(shí)現(xiàn)

內(nèi)核驅(qū)動(dòng)程序因?yàn)樾枰筒僮飨到y(tǒng)進(jìn)行大量的交互，因此其程序內(nèi)部包含有大量的函數(shù)調(diào)用，這些函數(shù)調(diào)用也是內(nèi)核驅(qū)動(dòng)程序?qū)崿F(xiàn)功能的必備條件，例如對(duì)于驅(qū)動(dòng)程序來(lái)說(shuō)，要完成PCI設(shè)備的注冊(cè)、使用及注銷(xiāo)行為，需要對(duì)Kernel接口函數(shù)進(jìn)行調(diào)用，因此本文對(duì)每個(gè)進(jìn)入和離開(kāi)Kernel的函數(shù)都進(jìn)行了插樁，以便確定其行為是否合法。

對(duì)于每一個(gè)函數(shù)的插樁遵循以下規(guī)則:直接在該函數(shù)尾部添加check進(jìn)行插樁，之所以用check進(jìn)行命名也是為了便于后續(xù)檢測(cè)規(guī)則進(jìn)行檢測(cè)。例如:網(wǎng)卡的注銷(xiāo)函數(shù)pci＿driver＿remove進(jìn)行插樁后命名為 pci＿driver＿remove＿check。

根據(jù)網(wǎng)卡驅(qū)動(dòng)的工作流程，我們制定如下的檢測(cè)規(guī)則，在網(wǎng)卡驅(qū)動(dòng)注冊(cè)前后分別進(jìn)行插樁，判定驅(qū)動(dòng)是否存在未經(jīng)注冊(cè)便調(diào)用的問(wèn)題。如下所示為網(wǎng)卡驅(qū)動(dòng)在調(diào)用內(nèi)核接口進(jìn)行注冊(cè)時(shí)的插樁實(shí)例。

因?yàn)閷⒃创a進(jìn)行插樁后，需要將其寫(xiě)入到Linux內(nèi)核驅(qū)動(dòng)中的相關(guān)模塊，并對(duì)整體進(jìn)行編譯，為了達(dá)成這樣的目的，我們需要利用標(biāo)準(zhǔn)C語(yǔ)言形式對(duì)其進(jìn)行插樁改寫(xiě)，同時(shí)為了保證插樁后的內(nèi)核驅(qū)動(dòng)源代碼可以得到正確的編譯執(zhí)行，因此改寫(xiě)形式也需要符號(hào)Linux系統(tǒng)內(nèi)核源碼的編寫(xiě)規(guī)則。

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

4.1 數(shù)學(xué)定義

傳統(tǒng)的符號(hào)執(zhí)行技術(shù)屬于靜態(tài)分析技術(shù)之一，但近年來(lái)改進(jìn)后的符號(hào)執(zhí)行技術(shù)也發(fā)展成為動(dòng)態(tài)分析技術(shù)的一種，本文對(duì)其進(jìn)行如下的數(shù)學(xué)定義。

我們定義被分析程序?yàn)镻，當(dāng)前路徑為 ρi，路徑條件為 δρi，程序運(yùn)行過(guò)程中的變量為var，在程序運(yùn)行過(guò)程中實(shí)際存儲(chǔ)為S，其存儲(chǔ)變量為Svar，符號(hào)存儲(chǔ)為F，其存儲(chǔ)變量為Fvar，路徑條件表達(dá)式為exp。

我們用一個(gè)數(shù)組定義程序的當(dāng)前狀態(tài)，定義程序P執(zhí)行的過(guò)程就是當(dāng)前狀態(tài)的更新過(guò)程，即該數(shù)組在程序執(zhí)行時(shí)一直處于變化狀態(tài)。

因?yàn)樯婕暗綄?shí)際運(yùn)行，在運(yùn)行過(guò)程中，實(shí)際值的運(yùn)算和符號(hào)值的運(yùn)算并存，因此定義三種命令:

定義1:ass為賦值語(yǔ)句，其形式為var≡exp；

定義2:con為條件語(yǔ)句，其形式為if exp then ins1，else ins2；

定義3:sto為停止語(yǔ)句。

則動(dòng)態(tài)符號(hào)執(zhí)行技術(shù)可以對(duì)其進(jìn)行如下的數(shù)學(xué)描述。

對(duì)該過(guò)程循環(huán)執(zhí)行，則所有路徑都會(huì)被執(zhí)行。在執(zhí)行過(guò)程中，持續(xù)手機(jī)約束條件，并通過(guò)約束求解[2]引擎進(jìn)行求解，最終可得到測(cè)試用例。

4.2 符號(hào)化設(shè)備

本文借助選擇性符號(hào)執(zhí)行引擎S2E[3]為基礎(chǔ)框架進(jìn)行改進(jìn)。S2E是在Klee[4]和Qemu的基礎(chǔ)上完成的符號(hào)執(zhí)行引擎，區(qū)別于普通的符號(hào)執(zhí)行技術(shù)，S2E結(jié)合了符號(hào)執(zhí)行技術(shù)和動(dòng)態(tài)分析技術(shù)，很有效的減少了路徑爆炸的問(wèn)題。

(1)發(fā)現(xiàn)

網(wǎng)卡設(shè)備是基本的PCI設(shè)備，每一個(gè)PCI設(shè)備都是通過(guò)pci＿dev結(jié)構(gòu)體進(jìn)行描述，對(duì)于一個(gè)新的PCI設(shè)備，Linux系統(tǒng)會(huì)根據(jù)PCI配置空間進(jìn)行設(shè)備的配置工作，我們要將設(shè)備符號(hào)化就需要讓Linux系統(tǒng)檢索到PCI配置空間，表2為根據(jù)網(wǎng)卡的特殊性構(gòu)造的配置空間信息。

表2 網(wǎng)卡配置空間信息

(2)I/O操作

對(duì)于I/O的符號(hào)化需要實(shí)現(xiàn)下述功能:只有產(chǎn)生讀操作(read)時(shí)，才返回符號(hào)值，否則不做處理。

I/O主要有兩種，一種是端口I/O，對(duì)應(yīng)著PCI端口I/O，這樣的操作一般借助inb、outb等硬件指令進(jìn)行訪問(wèn)存儲(chǔ)操作。因此本文對(duì)S2E引擎中的inb、outb等硬件指令進(jìn)行修改，對(duì)于inb類(lèi)操作則返回符號(hào)值，該符號(hào)值等于指令相應(yīng)字節(jié)大小。

當(dāng)函數(shù)的輸入值是I/O空間地址時(shí)，內(nèi)核驅(qū)動(dòng)程序借助調(diào)用inb來(lái)修改保存在該空間地址的數(shù)據(jù)，而當(dāng)符號(hào)化設(shè)備時(shí)，指令返回的數(shù)據(jù)標(biāo)記為返回值長(zhǎng)度的符號(hào)值，即實(shí)現(xiàn)了符號(hào)化I/O。

還有一種是內(nèi)存映射I/O，對(duì)應(yīng)著PCI內(nèi)存。本文對(duì)S2E引擎進(jìn)行如下修改，當(dāng)Linux內(nèi)核中映射函數(shù)被調(diào)用時(shí)，在S2E引擎中標(biāo)記該地址空間范圍，如果有對(duì)該地址空間進(jìn)行訪問(wèn)存儲(chǔ)的指令時(shí)，只對(duì)讀操作返回符號(hào)值，當(dāng)內(nèi)存映射接觸后，也同時(shí)刪除S2E中的標(biāo)記。

(3)中斷

網(wǎng)卡設(shè)備存在大量的中斷操作，因此，在符號(hào)化設(shè)備時(shí)，必須要提供中斷操作的機(jī)制。借助S2E所提供的各種插件，我們可以對(duì)中斷進(jìn)行模擬。

當(dāng)Raw監(jiān)視器插件接收到系統(tǒng)運(yùn)行過(guò)程中我們所關(guān)注的驅(qū)動(dòng)在加載的信號(hào)時(shí)，向模塊執(zhí)行檢測(cè)插件發(fā)信號(hào)，同時(shí)函數(shù)監(jiān)視器插件也會(huì)發(fā)出信號(hào)，兩種信號(hào)由庫(kù)函數(shù)調(diào)用插件捕獲并最終交由Qemu虛擬機(jī)的中斷觸發(fā)函數(shù)觸發(fā)中斷。

(4)DMA

與符號(hào)化I/O類(lèi)似，針對(duì)讀(read)操作返回符號(hào)值，否則不處理。

當(dāng)內(nèi)核驅(qū)動(dòng)程序向系統(tǒng)申請(qǐng)DMA映射時(shí)，S2E獲取映射的具體信息，包括映射的虛擬地址的大小及地址起始值等，獲取這些信息后，S2E將該地址空間標(biāo)識(shí)為DMA映射區(qū)域。如果針對(duì)該地址空間產(chǎn)生了讀操作，S2E會(huì)首先判斷此時(shí)CPU是否對(duì)該地址空間擁有控制權(quán)，是的話返回符號(hào)值，否則不處理。而當(dāng)內(nèi)核驅(qū)動(dòng)程序需要取消DMA映射時(shí)，S2E則會(huì)將標(biāo)識(shí)取消。這樣就實(shí)現(xiàn)了符號(hào)化DMA。

5 結(jié)果與分析

5.1 原型系統(tǒng)

脆弱性分析原型系統(tǒng)基本結(jié)構(gòu)如圖5所示。

圖5 原型系統(tǒng)設(shè)計(jì)結(jié)構(gòu)

整個(gè)框架如圖5所示，對(duì)代碼進(jìn)行插樁后將編譯后的源碼運(yùn)行在Qemu虛擬機(jī)中以便進(jìn)行整體監(jiān)控，程序具體執(zhí)行時(shí)，其進(jìn)入和退出內(nèi)核時(shí)會(huì)進(jìn)行判定，如果該條路徑存在檢測(cè)規(guī)則，則對(duì)規(guī)則進(jìn)行檢測(cè)，否則正常執(zhí)行。而S2E引擎提供了符號(hào)化設(shè)備，在內(nèi)核驅(qū)動(dòng)程序需要具體的硬件設(shè)備進(jìn)行輸入時(shí)，通過(guò)符號(hào)化設(shè)備來(lái)完成內(nèi)核驅(qū)動(dòng)程序與硬件設(shè)備的交互工作。

5.2 結(jié)果

實(shí)現(xiàn)環(huán)境如表3所示。

表3 實(shí)驗(yàn)環(huán)境

發(fā)現(xiàn)e1000存在非法調(diào)用脆弱性，結(jié)果如下:

根據(jù)上文所介紹的內(nèi)核驅(qū)動(dòng)程序的運(yùn)行規(guī)則，一般先使用register函數(shù)進(jìn)行設(shè)備的注冊(cè)，才可以繼續(xù)調(diào)用其它函數(shù)實(shí)現(xiàn)驅(qū)動(dòng)所需要的相關(guān)功能。而在e1000驅(qū)動(dòng)中的e1000＿main.c文件，其中存在未經(jīng) register＿netdev函數(shù)注冊(cè)，便調(diào)用 netif＿carrier＿off函數(shù)。

發(fā)現(xiàn)benet崔在非法調(diào)用脆弱性，結(jié)果如下:

根據(jù)上文所介紹的內(nèi)核驅(qū)動(dòng)程序的運(yùn)行規(guī)則，一般先使用register函數(shù)進(jìn)行設(shè)備的注冊(cè)，才可以繼續(xù)調(diào)用其它函數(shù)實(shí)現(xiàn)驅(qū)動(dòng)所需要的相關(guān)功能。而在benet驅(qū)動(dòng)中的be＿main.c文件，其中存在未經(jīng) register＿netdev函數(shù)注冊(cè)，便調(diào)用 netif＿carrier＿off函數(shù)。

6 結(jié)語(yǔ)

本文通過(guò)分析網(wǎng)絡(luò)設(shè)備驅(qū)動(dòng)程序的基本功能模塊，提出了規(guī)則檢查的原型系統(tǒng)設(shè)計(jì)思路，利用符號(hào)執(zhí)行工具的優(yōu)點(diǎn)，基于其實(shí)現(xiàn)了原型系統(tǒng)，并對(duì)具體的網(wǎng)卡驅(qū)動(dòng)進(jìn)行測(cè)試，實(shí)驗(yàn)表明，該系統(tǒng)可以有效快速的發(fā)現(xiàn)脆弱性。

[1]Chou A，Yang J，Chelf B，et al.An Empirical Study of Operating Systems Eerrors[J].Proc of the 8th ACM Symposium on Operating System Principles，2001:73－88.

[2]季曉慧，張健.約束問(wèn)題求解[J].自動(dòng)化學(xué)報(bào)，2007(2):125－131.

[3]Chipounov V，Kuznetsov V，Candea G.S2E:A Platform for In－Vivo Multi－Path Analysis of Software Systems[J].ACM SIGARCH Computer Architecture News，2012.39(1):265－278.

[4]Cadar C，Dunbar D，Engler D.KLEE:Unassisted and Automatic Generation of High－Coverage Tests for Complex Systems Programs[C]//Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation.USENIX Association，2008:209－224.

Research on Net－Driver Vulnerability based on Rules Checking

HE Hao，XIA Qun－feng，GAN Shui－tao
(Lab of Computer Science，Jiangnan Computer Technique Institute，Wuxi Jiangsu 214000，China)

In a computer system，the driver serves as an interaction bridge of between operating system and underlying hardware，and thus its validity should not be ignored.By taking the Linux kernel net－driver as the major object，through analysis on the basic functionmodule of net drivers，and with the help of symbolic execution，an analysismethod based on rules checking for net drivers is proposed，and a automatic analysis system constructed.For Linux kernel2.6.29 version，the proposed system is used to carry out test，and the result shows that this system can find new vulnerability quickly and efficiently.

net driver； vulnerability； symbolic execution； rules checking

TP311

A

1009－8054(2016)06－0083－05

2016－03－06

賀 灝(1991—)，男，碩士，主要研究方向?yàn)榫W(wǎng)絡(luò)安全；

夏群峰(1980—)，男，碩士，工程師，主要研究方向?yàn)榫W(wǎng)絡(luò)安全；

甘水滔(1986—)，男，博士，工程師，主要研究方向?yàn)榫W(wǎng)絡(luò)安全。