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

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

struct tnum {
    u64 value;
    u64 mask;
}

第二個(gè)是值的有效范圍，作為帶符號(hào)和無(wú)符號(hào)的 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ì)算機(jī)擁有過(guò)多的內(nèi)存，檢驗(yàn)器可以直接使用通用集合數(shù)據(jù)結(jié)構(gòu)來(lái)跟蹤可能值的集合。這種方法的缺點(diǎn)是與存儲(chǔ) bpf_reg_state 所需的字節(jié)相比，內(nèi)存開(kāi)銷(xiāo)會(huì)顯著增加。更有效方法的缺點(diǎn)是它不能表示所有可能的集合，因此有時(shí)代碼需要進(jìn)行保守的過(guò)近似（conservative over-approximation），這會(huì)像滾雪球一樣，導(dǎo)致檢驗(yàn)器無(wú)法找出理論上本可以找到的邊界。例如，檢驗(yàn)器當(dāng)前無(wú)法處理不連續(xù)范圍，例如必須介于 1 到 4 或 8 到 10 之間的值。相反，它會(huì)將范圍跟蹤為僅從 1 到 10。

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

跟蹤更少的邊界值

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

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

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

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

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

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

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

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