KernelScript：用型別把 eBPF 的三塊接起來

KernelScript 是一個 DSL——它把一個 eBPF 應用原本分散在三個地方的原始碼（kernel 程式、userspace loader、兩邊共用的 map）收進同一份原始碼、同一套型別系統，再編譯成標準 C，透過既有的 libbpf 工具鏈載入與驗證。這個判斷不是「eBPF 需要另一個更嚴格的 verifier」，而是「eBPF 需要把散落在三個地方的型別事實收回同一個地方」——KernelScript 選的不是加強 runtime 的檢查，是把檢查提前到 compile time，而且要求它一次涵蓋三塊，不是一個一個去補。

三塊分裂的程式設計模型

一個 eBPF 應用實際上橫跨三塊。kernel 端是編譯進 BPF bytecode、要通過 verifier 才能載入的程式本體；userspace 端是負責把這支程式塞進 kernel、設定好 attach 點的 loader，通常就是 libbpf；中間是兩邊都要碰的共用 map——kernel 程式寫入、userspace 讀出，或者反過來。三塊各自有自己的原始碼、自己的建置流程，只在執行期透過 map fd、prog fd 這些數字打交道。論文對這個現象的說法很直接：「a single application spans kernel code, a userspace loader, and shared maps, yet the relationships among these pieces go unchecked」——程式設計模型本身就是碎的，而碎片之間的關係不被檢查。

值得先講清楚 verifier 到底管到哪裡。eBPF 的 verifier 確實嚴格，它在執行前就證明程式不會讓 kernel crash——這是 eBPF 敢把使用者程式碼放進 kernel 空間跑的前提。但那個證明只涵蓋 kernel 端這一塊自己的記憶體安全、控制流；它不涵蓋「這個 map 是不是真的這個型別」「這個 program handle 是不是真的能在這個情境被呼叫」這種橫跨三塊的資訊。verifier 對 kernel 程式本身很挑剔，對 kernel 程式跟另外兩塊之間的關係完全不聞不問。

這種「只靠數字打交道」的耦合方式，在系統設計上其實很常見——不同語言、不同 process 之間本來就得靠 fd、控制碼這類不透明的識別碼溝通，這本身不是問題。問題是 eBPF 的三塊明明共用同一份原始意圖：同一個 map、同一支程式，卻被迫用最不透明的方式互相指涉，型別資訊反而在傳遞的過程裡消失了。靠文件或註解手動同步兩邊的宣告不是沒人試過，只是文件不會被編譯器檢查，註解過期了也不會有任何工具提醒你。三塊天生要分開建置也有其道理——kernel 程式要通過 verifier、被編進 BPF bytecode；userspace loader 是一支普通的原生程式，走一般的編譯器、一般的連結流程；兩者的建置目標、甚至工具鏈本身都不一樣。KernelScript 沒有打算合併這兩條建置路徑，它合併的只是「型別在哪裡被宣告」這件事——建置仍然分兩條走，宣告只寫一次。

沒人替你檢查的跨界關係

跨界關係不被檢查，具體長什麼樣？最直接的例子就是 map 或 event 的型別。同一個 map，kernel 程式那邊宣告一次 key/value 型別，userspace loader 那邊各自再宣告一次——C 語言不會替你比對這兩份宣告是否一致，libbpf 也不會。兩邊只要在執行期對得上 map fd 這個數字，build 就過、load 也過。論文把後果講得很白：「A map or event type defined differently on each side silently corrupts shared state.」不是編譯失敗，不是載入失敗，是執行期悄悄把資料寫壞或讀錯——而且沒有任何錯誤訊息提醒你哪裡對不上。

這也是為什麼論文把問題定調成「重複」而不是「複雜」。KernelScript 的論點是：「these cross-boundary relationships duplicate information that a type system can unify」——map 的 key/value 型別、event 的 payload 型別、哪個 program handle 能在哪個情境被呼叫，這些事實本來只需要講一次，卻被迫在 kernel 程式、userspace loader 兩份原始碼裡各自宣告一次。兩份宣告本質上是同一個事實，只是被人手動抄了兩遍——手動抄兩遍的東西，遲早會抄不一致。

這個失敗模式特別麻煩的地方在於，它不像記憶體越界那樣會讓程式明顯掛掉，而是產生「看起來正常，其實讀寫錯位」的資料。對 observability、networking 這類直接影響 production 資料正確性的 eBPF 應用來說，這種悄悄的錯位往往要等到下游資料對不上、或者排查很久之後才會被人發現，除錯成本比一次乾脆的 crash 高得多——crash 至少會留下一支 stack trace，型別錯位往往什麼痕跡都不留。這也是為什麼「靠更仔細的 code review」不是可靠的解法：review 能抓到的是「這次改動看起來合理」，卻很難逐行比對兩份分屬不同語言、不同檔案的型別宣告是否逐位元組一致——這件事本來就更適合交給機器做，而不是靠人眼在兩個分頁之間來回核對。

型別怎麼把三塊縫起來：maps、program handles、execution domains

KernelScript 把三種東西的型別放進同一份原始碼裡宣告。第一種是 map——key/value 型別對編譯器只可見一次，kernel 程式跟 userspace loader 端都從同一份宣告取用，不再各自抄一份。第二種是 program handle——從名稱上看，是把一支已載入的 eBPF 程式當成型別化的參照來使用，而不是一個沒有型別資訊的裸 fd 整數，讓呼叫方跟被呼叫方的期待可以在編譯期被比對（這部分屬於根據命名的合理推斷，論文摘要本身沒有進一步展開實作細節）。第三種是 execution domain——XDP、TC、kprobe、tracepoint、struct_ops 各自是不同的執行語境，一段程式碼寫在哪個語境下才有效，由型別系統知道，而不是靠工程師記在腦子裡。

三者共用同一套型別系統的直接後果是：任何一邊改了型別，另一邊沒跟著改，編譯器在編譯期就能發現，不用等到跑起來才炸。論文原句是：「We present KernelScript, a DSL that types maps, program handles, and execution domains in one source」——「in one source」是關鍵字，不是「有一套規範建議大家遵守」，而是同一份原始碼、同一次型別檢查，物理上不給兩份宣告分岔的機會。

把三塊收進同一份原始碼，另一個直接影響是 code review 的單位跟著改變。以前 reviewer 要同時盯著 kernel 程式的 diff 跟 userspace loader 的 diff，自己在腦子裡比對兩邊的型別有沒有對齊；現在這件事變成編譯器的工作，reviewer 只需要看一份 diff、關注邏輯本身，而不是充當人肉型別比對器。execution domain 這一種型別尤其值得留意——XDP、TC、kprobe、tracepoint、struct_ops 各自的執行語境差異很大，一支寫給 tracepoint 的邏輯被誤用在 XDP 情境下，後果不會只是型別對不上，還牽涉到能不能存取的資料、能不能呼叫的 helper 完全不同；把這件事交給型別系統記，比要求每個工程師背熟五種語境的差異更可靠。

編回標準 C：為什麼不重寫工具鏈

KernelScript 沒有另起爐灶做一個新的 runtime 或新的 verifier。它把整份型別化的原始碼編譯成標準 C，再交給原本那條 libbpf 工具鏈——一樣的 verifier、一樣的 loader、一樣的除錯與追蹤工具。論文的描述是「then compiles to standard C through the original toolchain」，評估段落又補了一句「generated code remains compatible with the existing toolchain」。這代表型別檢查完全是編譯期加上去的一層，不影響、也不需要 kernel 端配合修改；產生出來的 C 程式碼理論上跟工程師手寫的版本一樣，可以被既有的 bpftool、libbpf 生態直接消化。

這個選擇把 KernelScript 的定位講得很清楚：它不是要取代 eBPF 的 runtime 模型，而是在原始碼層加一道編譯期的型別關卡，把本來要靠 code review、靠踩過雷才能對齊的三塊資訊，收進一個編譯器就能檢查的地方。verifier 依然是那個 verifier，libbpf 依然是那個 libbpf——KernelScript 賭的是「在它們前面多一層型別檢查」比「換掉它們」風險小得多，也更容易被既有專案採用。

這對想要導入的團隊也是關鍵。既有的除錯工具鏈——bpftool 檢視 map 內容、libbpf 的載入診斷訊息、既有的 CI 流程——完全不用換掉；KernelScript 帶來的是編譯期多一道關卡，不是要求團隊放棄原本熟悉的觀測與除錯手段。採用成本因此被壓在「換一套原始碼語言、學一套型別系統」，而不是「換一整條維運鏈路、賭上 kernel 相容性」。verifier 的角色也完全沒有變：它照樣是那最後一道、對記憶體安全和控制流極度嚴格的關卡，KernelScript 只是在它之前多插了一關，兩層各管各的，不互相取代。

把型別系統疊在既有的低階目標語言之上、再編譯下去，不是 KernelScript 發明的手法——TypeScript 疊在 JavaScript 之上、不少 formally-verified 系統疊在 C 之上，走的都是同一條路：不改動底層的執行語意，只在原始碼層多驗證一次，讓舊的執行環境完全不用感知這層新增的檢查。KernelScript 特別的地方在於它疊加的範圍橫跨兩個地址空間、三種原始碼形態，而不只是單一語言內部的型別加強。這也是為什麼「相容既有工具鏈」在這裡格外重要——這類方案一旦要求使用者連 runtime、連 kernel 版本都一起換掉，導入門檻會高得多，願意嘗鮮的團隊也會少得多。

43 個 workload 上的答案

評估涵蓋 XDP、TC、kprobe、tracepoint、struct_ops 五種 execution domain，共 43 個 eBPF workload。KernelScript 在編譯期擋下了標準 C/libbpf 組合「照樣 build、照樣 load」的跨界 bug——同樣的錯誤在原本的工具鏈下不會有任何警告。把三塊原始碼收進一份型別化來源後，跨界改動（例如改一個 map 的型別、改一個 event 的 payload）需要動的 diff 也縮小到原本的五分之一；同時，產生出來的 C 程式碼與既有工具鏈維持相容，不需要 kernel 端配合任何修改。論文原句是：「KernelScript rejects cross-boundary bugs at compile time that standard C/libbpf still builds and loads, a unified source shrinks the diffs for cross-boundary changes by 5x, and generated code remains compatible with the existing toolchain.」

五分之一的 diff 差距，直觀的來源是「要動的地方變少」。標準 C/libbpf 底下，改一個跨界型別通常要同時動三份原始碼：kernel 程式裡對 map 的使用、共用的型別宣告（header 或 skeleton）、userspace loader 裡對應的宣告。KernelScript 把這三份收進一份原始碼後，理論上只要改一處。下面用示意圖呈現這個差距的形狀——不是逐行從論文量出來的數字，只是把「三處」與「一處」的對比畫出來，對應論文量到的整體 5 倍差距。

43 個 workload、五種 execution domain 的覆蓋範圍，回應了一個對這類方案常見的疑慮——「加一層型別系統」的做法，往往在玩具範例上好看，碰到真實碼庫的複雜度就失靈。論文選擇橫跨 XDP、TC、kprobe、tracepoint、struct_ops 做評估，至少說明這套型別系統不是只為單一種 attach 語境量身打造，而是刻意涵蓋 eBPF 生態裡幾種行為差異最大的執行語境；五分之一的 diff、擋下編譯期本可發現的跨界 bug，這兩個結果是在這個橫跨五種語境的樣本上量出來的，而不是單一 use case 的個案。至於這 5 倍差距在長期維護上意味著什麼，論文本身沒有進一步展開——但對任何維護過雙端同步的工程師來說，「改動的地方變成五分之一」直接對應的是「漏改一處的機率也大致等比例下降」，這是型別系統把重複資訊收攏之後最直接的副作用。

對正在維護中大型 eBPF 專案的團隊來說，這個結果的參考點不是「要不要立刻換語言」，而是「跨界型別錯位」這個問題本身值不值得認真對待。如果一個團隊的 map 型別、event payload 型別經常需要在 kernel 程式跟 loader 之間手動同步，KernelScript 至少證明了：把這件事交給編譯器，在橫跨五種執行語境的 43 個 workload 上是可行的，而且省下來的不只是擋下幾個 bug，還有跨界改動時實際要動的程式碼量。

這個設計解鎖了什麼：跨界型別錯誤不用等到踩雷才被人肉抓到——KernelScript 把本來要靠 code review 對齊的三塊資訊收進一個編譯器就能檢查的地方，而且不必為此換掉整條 eBPF 工具鏈，產生的 C 程式碼照樣走原本的 verifier 與 libbpf。