LWN：簡化BPF verifier！

關(guān)注了就能看到更多這么棒的文章哦～

Simplifying the BPF verifier

By Daroc Alden
June 13, 2024
LSFMM+BPF
Gemini-1.5-flash translation
https://lwn.net/Articles/977815/

BPF 檢驗器 (BPF Verifier) 是一個復(fù)雜的程序。很不幸，這導(dǎo)致了相關(guān)的貢獻(xiàn)者在開發(fā)它時更加困難，同時也更容易出現(xiàn)未知的 bug。Yu Shung-Hsi 在 2024 年的 Linux 存儲、文件系統(tǒng)、內(nèi)存管理和 BPF 峰會 上提出了兩個具體建議，旨在簡化檢驗器，使其更容易維護(hù)。Yu 建議改變檢驗器中跟蹤部分已知值的機(jī)制，并清理接口，以隱藏值跟蹤器（value-tracker）內(nèi)部表示的細(xì)節(jié)。

檢驗器的核心功能之一是值跟蹤——推斷變量可能持有的值的集合，以確保訪問保持在邊界內(nèi)。由于任何值都可能用于計算數(shù)組索引或檢驗器感興趣的其他內(nèi)容，因此值跟蹤器需要跟蹤程序中的每個值。檢驗器在 bpf_reg_state 結(jié)構(gòu)中存儲有關(guān)可能值的的信息，該結(jié)構(gòu)跟蹤兩種相關(guān)的信息。第一個是“已知位（known bits）”，它使用掩碼來指示哪些 bit 的值是精確知道的：

struct tnum {
    u64 value;
    u64 mask;
}

第二個是值的有效范圍，作為帶符號和無符號的 32 位和 64 位量進(jìn)行跟蹤：

struct bpf_reg_state {
    ...
    struct tnum var_off;
    s64 smin_value; /* 最小可能 (s64) 值 */
    s64 smax_value; /* 最大可能 (s64) 值 */
    u64 umin_value; /* 最小可能 (u64) 值 */
    u64 umax_value; /* 最大可能 (u64) 值 */
    s32 s32_min_value; /* 最小可能 (s32) 值 */
    s32 s32_max_value; /* 最大可能 (s32) 值 */
    u32 u32_min_value; /* 最小可能 (u32) 值 */
    u32 u32_max_value; /* 最大可能 (u32) 值 */
}

選擇要跟蹤哪些信息，就代表了準(zhǔn)確性和效率之間的權(quán)衡。如果計算機(jī)擁有過多的內(nèi)存，檢驗器可以直接使用通用集合數(shù)據(jù)結(jié)構(gòu)來跟蹤可能值的集合。這種方法的缺點是與存儲 bpf_reg_state 所需的字節(jié)相比，內(nèi)存開銷會顯著增加。更有效方法的缺點是它不能表示所有可能的集合，因此有時代碼需要進(jìn)行保守的過近似（conservative over-approximation），這會像滾雪球一樣，導(dǎo)致檢驗器無法找出理論上本可以找到的邊界。例如，檢驗器當(dāng)前無法處理不連續(xù)范圍，例如必須介于 1 到 4 或 8 到 10 之間的值。相反，它會將范圍跟蹤為僅從 1 到 10。

在實踐中，跟蹤已知位和可能范圍提供了良好的權(quán)衡。單獨使用其中任何一個都無法捕獲檢驗器關(guān)心的重要屬性，但它們在一起的大小和復(fù)雜度并不太大，可以一起使用。它們可以表示可能的值集，例如“0 到 64 之間的 8 的倍數(shù)”，這非常適合跟蹤數(shù)組訪問的對齊和邊界。

跟蹤更少的邊界值

Yu 提出了一項建議，可以在保持相同精度的情況下，顯著簡化 bpf_reg_state 的實際實現(xiàn)：不再專門跟蹤帶符號數(shù)的范圍?，F(xiàn)在，無論何時檢驗器更新一個范圍（例如從條件分支推斷新的 smin_value ），它都需要執(zhí)行復(fù)雜的同步動作，以確保更改反映在每個范圍內(nèi)。Yu 說，目前，這種同步動作涉及在 20 個不同方向上傳播信息。這是因為代碼沒有跟蹤哪些字段已更新，因此在處理代碼塊后同步邊界的過程中就需要把來自五個在跟蹤的約束（四個范圍和一個 tnum ）中的每一個的信息都共享給其他四個。

Yu 建議，不要以當(dāng)前的方式跟蹤范圍，而是使用他 在 2023 年 10 月討論 的方法的變體來跟蹤范圍。本質(zhì)上，允許最大值小于最小值。以這種方式表示的范圍始終從最小值開始，到最大值結(jié)束，但它可能會在途中環(huán)繞。這意味著范圍（最小值：0xFFFFFFFC，最大值：4）表示帶符號范圍（-4, 4），同時表示/無符號/范圍（0xFFFFFFFC, UINT32_MAX）和（0, 4）?，F(xiàn)有代碼不處理這樣的不連續(xù)范圍，因此 Yu 計劃添加一些轉(zhuǎn)換函數(shù)，將新的表示方式轉(zhuǎn)換為舊代碼使用。

以這種方式存儲范圍有一些好處。最大的好處是，無需同步帶符號和無符號邊界的信息——它們會自動同步，完全依靠表示方式本身。這也減少了檢驗器在已知位表示和范圍表示之間需要傳播的信息量，將代碼減少到只有六個信息流方向（從三個邊界中的每一個到另外兩個）。Yu 希望這將使處理值跟蹤的檢驗器代碼更容易使用，也更容易正式驗證。

Yu 計劃分幾個步驟將這些更改引入上游；最初，將實現(xiàn)轉(zhuǎn)換函數(shù)，而主要的檢驗器代碼將基本保持不變。然后，他計劃更改數(shù)值跟蹤代碼中最關(guān)鍵的部分，原生使用新的表示方式，然后調(diào)整內(nèi)核氣動過程。最后，可以刪除最后一處使用以及轉(zhuǎn)換函數(shù)。

Yu 簡化值跟蹤器的第二個建議是為處理 tnum 和范圍值引入一個更抽象的接口。這些建議可以獨立實現(xiàn)，但它們肯定可以相互補(bǔ)充。Yu 說，現(xiàn)在，在檢驗器代碼上工作需要了解 tnum 和范圍的內(nèi)部細(xì)節(jié)；但對這些值執(zhí)行的最常見操作只是取交集或者包含檢查。如果將它們提取到它們自己的函數(shù)中，那么實際的值跟蹤代碼的大部分可以大大簡化。

然而，這些并不是簡化檢驗器維護(hù)的唯一方法。會議以討論如何改進(jìn)文檔、檢驗器的哪些方面可以標(biāo)準(zhǔn)化以及這些建議將如何影響正式驗證而結(jié)束。檢驗器無疑已經(jīng)因為它的難以維護(hù)而知名了，但似乎內(nèi)核的 BPF 開發(fā)人員有一個計劃來開始改變這種狀況。

全文完
LWN 文章遵循 CC BY-SA 4.0 許可協(xié)議。

長按下面二維碼關(guān)注，關(guān)注 LWN 深度文章以及開源社區(qū)的各種新近言論～