Precise and Scalable Detection of Double-Fetch Bugs in OS Kernels

開源項(xiàng)目地址：https://github.com/sslab-gatech/deadline

本文發(fā)表于IEEE S&P 2018，作者是Meng Xu, Chenxiong Qian, Kangjie Lu, Michael Backes, Taesoo Kim。第一作者M(jìn)eng Xu來(lái)自佐治亞理工學(xué)院。本文的第四作者M(jìn)ichael Backes為CISPA亥姆霍茲信息安全中心主席兼創(chuàng)會(huì)理事。

主要內(nèi)容

操作系統(tǒng)的系統(tǒng)調(diào)用執(zhí)行期間，操作系統(tǒng)內(nèi)核可能會(huì)多次讀取同一塊用戶空間的內(nèi)存（multi-read）。如果在兩次讀取之間，用戶空間內(nèi)存由于條件競(jìng)爭(zhēng)等原因使數(shù)據(jù)發(fā)生了變化，則可能導(dǎo)致double-fetch bug。前人工作中曾嘗試通過(guò)靜態(tài)或動(dòng)態(tài)方法來(lái)檢測(cè)這種bug，然而由于對(duì)double-fetch沒(méi)有準(zhǔn)確的定義，這些工作會(huì)導(dǎo)致大量的誤報(bào)和漏報(bào)，還需要引入大量的人工分析。

本文首先對(duì)double-fetch進(jìn)行了正式和準(zhǔn)確的定義，并設(shè)計(jì)實(shí)現(xiàn)靜態(tài)分析工具——DEADLINE來(lái)自動(dòng)化檢測(cè)系統(tǒng)內(nèi)核中的double-fetch bug。DEADLINE使用靜態(tài)分析系統(tǒng)性地找到內(nèi)核中的multi-read行為，并使用符號(hào)化檢測(cè)確認(rèn)multi-read行為是否是double-fetch bug。DEADLINE發(fā)現(xiàn)了在Linux內(nèi)核中的23個(gè)新bug和FreeBSD內(nèi)核中的1個(gè)新bug。之后，作者基于自身經(jīng)驗(yàn)及與內(nèi)核開發(fā)者的交流，總結(jié)了4個(gè)patch和預(yù)防double-fetch的策略。

形式化定義

作者在定義double-fetch之前，先對(duì)其相關(guān)概念進(jìn)行了定義：

Fetch：對(duì)于一次fetch操作，使用一個(gè)(A,S) 二元組來(lái)表示本次操作的屬性，其中A表示讀取數(shù)據(jù)的地址，S表述數(shù)據(jù)的大小

Overlapped-fetch：對(duì)于兩次不同的Fetch (A₀, S₀) 和 (A₁, S₁)，若滿足A₀ <= A₁ < A₀ + S₀ or A₁ <= A₀ < A₁ + S₁的關(guān)系，則稱兩次fetch為overlapped-fetch。其中重疊部分表示為(A₀₁, S₀₁)，并用三元組 (A₀₁, S₀₁, i = [0,1])來(lái)分別表示兩次fetch中讀取的重疊數(shù)據(jù)部分。

控制依賴：對(duì)于一個(gè)變量V∈（A₀₁,S₀₁, 0），若V在第二次fetch之前受一組約束條件[Vc]的約束，則認(rèn)為V與（A₀₁,S₀₁）間存在控制依賴。若要證明在此情況下不存在double-fetch bug，必須證明第二次fetch中的V’∈（A₀₁,S₀₁, 1）滿足約束條件[Vc].

數(shù)據(jù)依賴：對(duì)于一個(gè)變量V∈（A₀₁,S₀₁, 0），若V在第二次fetch之前被消耗（例如賦值給其他變量，進(jìn)行了計(jì)算相關(guān)操作，作為參數(shù)傳入函數(shù)調(diào)用），則認(rèn)為V與（A₀₁,S₀₁）間存在數(shù)據(jù)依賴。若要證明在此情況下不存在double-fetch bug，必須證明第二次fetch中的V’∈（A₀₁,S₀₁, 1）滿足V==V’.

作者認(rèn)為，double-fetch bug遵循以下四個(gè)條件：

1. 至少有兩次對(duì)用戶空間的讀取操作，即double-fetch的前提是multi-read。用戶空間的讀取操作可以通過(guò)copy_from_user等傳遞函數(shù)進(jìn)行識(shí)別。

2. 兩次讀取的內(nèi)容必須存在重疊部分。即兩次fetch存在overlapped-fetch區(qū)域。

3. 兩次讀取的重疊部分必須有一定的關(guān)聯(lián)，可以是數(shù)據(jù)依賴或控制依賴。

4. 不能被證明兩次讀取的重疊部分在兩次讀取中是相同的。即用戶空間可以通過(guò)條件競(jìng)爭(zhēng)在兩次讀取之間修改重疊部分的值。

Figure 1 double-fetch示例

如上圖所示，perf_copy_attr_simplified函數(shù)內(nèi)部進(jìn)行了兩次fetch，第一次fetch從uattr中拷貝了4個(gè)字節(jié)的數(shù)據(jù)到size中，即F1（A=uattr, S=4）；第二次fetch從uattr中拷貝了size長(zhǎng)度的數(shù)據(jù)到attr中， 即F2（A=uattr，S=size）。這顯然是一次multi-read。兩次fetch操作都以u(píng)attr為起始地址，數(shù)據(jù)重疊區(qū)域?yàn)椋ˋ=uattr，S=4），因此兩次fetch滿足overlapped-fetch條件。圖中11-14行代碼可以看到，第一次fetch所得的變量size受一組條件約束，且變量size與第二次fetch的得到的attr->size重疊，即重疊區(qū)域存在控制依賴，需要證明其的約束條件一致。然而attr->size沒(méi)有受到任何條件的約束，無(wú)法證明兩次fetch的重疊部分相同，因此認(rèn)為這是一個(gè)double-fetch bug。

工具設(shè)計(jì)

DEADLINE首先使用靜態(tài)分析收集內(nèi)核代碼中的multi-read操作，并對(duì)每一組有關(guān)聯(lián)的multi-read進(jìn)行符號(hào)化執(zhí)行檢查（符號(hào)化執(zhí)行在LLVM IR層面上進(jìn)行），確定是否滿足double-fetch的上述形式化定義。如果是，則將其加入輸出集合。

收集multi-read

首先，掃描內(nèi)核代碼，通過(guò)識(shí)別代碼中的copy_from_user等讀取用戶空間數(shù)據(jù)的傳遞函數(shù)找到所有的fetch操作（如Figure 1所示）；其次，對(duì)于每個(gè)fetch操作所在的函數(shù)內(nèi)部，進(jìn)行函數(shù)內(nèi)的自底向上分析，以找到一個(gè)fetch pair（如Figure 2所示）。如果找到了一個(gè)fetch pair，則說(shuō)明找到了一個(gè)multi-reads操作，并將其用一個(gè)三元組<F0, F1, Fn>表示。在這個(gè)三元組中，F(xiàn)0和F1分別表示兩次fetch指令的位置，F(xiàn)n表示這兩條指令所在的函數(shù)名稱。如果在分析的過(guò)程中遇到了帶有fetch操作的函數(shù)，則會(huì)將這個(gè)函數(shù)代碼內(nèi)聯(lián)進(jìn)來(lái)進(jìn)行分析。

Figure 2 查找Fetch操作

Figure 3 收集fetch pair

從multi-read到double-fetch bug

前人的一些論文中的工具大都止步于找到內(nèi)核中的multi-reads情況，之后采用人工分析來(lái)確定double-fetch的bug，需要耗費(fèi)大量的人力。本文設(shè)計(jì)的工具在發(fā)現(xiàn)multi-reads之后，將繼續(xù)使用符號(hào)執(zhí)行構(gòu)建約束進(jìn)行求解，來(lái)進(jìn)行靜態(tài)分析，看multi-read是否滿足形式化定義中的四個(gè)條件，從而求解是否存在double-fetch bug。

Figure 4 符號(hào)化執(zhí)行檢查案例

文中給出了一個(gè)完整的案例分析，如Figure3所示。首先將函數(shù)參數(shù)和全局變量轉(zhuǎn)變?yōu)榉?hào)化表述形式，作為根SR（symbolic representation），之后將其他指令轉(zhuǎn)化為符號(hào)化表述。符號(hào)化的過(guò)程中，遇到與fetch數(shù)據(jù)相關(guān)的條件分支判斷，則將其轉(zhuǎn)化為assert斷言作為條件約束之一。兩次fetch之后，使用前述對(duì)double-fetch的形式化定義來(lái)插入約束并求解：即先判斷兩次所fetch的數(shù)據(jù)是否有重疊，再判斷在函數(shù)內(nèi)是否可以證明兩次fetch的數(shù)據(jù)重疊部分是相同的。在這個(gè)案例中，由于兩次fetch分別被標(biāo)識(shí)為U0和U1，且沒(méi)有約束證明兩者是相同的，故約束求解失敗，DEADLINE得出檢測(cè)結(jié)果，即此處存在double-fetch bug。

評(píng)估及討論：

DEADLINE在Linux和freeBSD中分別發(fā)現(xiàn)了23個(gè)和1個(gè)新的double-fetch bud。這些bug中的一些已經(jīng)與開發(fā)者進(jìn)行溝通并修補(bǔ)，有兩個(gè)被開發(fā)者標(biāo)注為“won’t fix”。

作者通過(guò)與開發(fā)者交流bug修復(fù)的過(guò)程，總結(jié)了一些關(guān)于預(yù)防double-fetch的緩解策略：

• 重寫：對(duì)于第二次fetch的數(shù)據(jù)中重疊部分，使用第一次fetch時(shí)讀取的數(shù)據(jù)進(jìn)行覆蓋；

• 檢測(cè)到數(shù)據(jù)變化就中止：如果檢測(cè)到兩次fetch數(shù)據(jù)不一致，則中止后續(xù)操作；

• 增量讀?。旱诙蝔etch時(shí)，跳過(guò)第一次fetch過(guò)的數(shù)據(jù)，以避免讀取重復(fù)數(shù)據(jù)；

• 重構(gòu)為一次性fetch：如果是控制依賴，則可以一次fetch所有的數(shù)據(jù)。

局限性

DEADLINE在以下幾個(gè)方面存在局限性：

1. 代碼覆蓋率：作者使用LLVM對(duì)內(nèi)核進(jìn)行編譯，對(duì)于沒(méi)有編譯成功的文件和沒(méi)有展開的宏代碼，將不會(huì)被測(cè)試覆蓋；

2. 路徑構(gòu)建：
   1）在函數(shù)內(nèi)構(gòu)建fetch-pair路徑時(shí)，限制了最大的路徑數(shù)（4096），如果兩次fetch超過(guò)了這個(gè)路徑長(zhǎng)度限制，則無(wú)法進(jìn)行分析；
   2）循環(huán)展開時(shí)僅展開一重循環(huán)，對(duì)于需要展開多次循環(huán)或跨循環(huán)的double-fetch bug無(wú)法分析；
   3）如果循環(huán)中有分支，僅會(huì)處理循環(huán)中的一條分支路徑，這種情況會(huì)有路徑遺漏。

3. 符號(hào)化執(zhí)行檢查：
   1）忽略了內(nèi)聯(lián)函數(shù)，假設(shè)其對(duì)符號(hào)執(zhí)行沒(méi)有影響；
   2）從指針到內(nèi)存對(duì)象的映射可能存在誤差；
   3）將約束檢查限制在封閉函數(shù)內(nèi)，對(duì)于在函數(shù)外進(jìn)行檢查的情況就會(huì)出現(xiàn)誤報(bào)。

文丨DR.XX, xcz, Wisher