使用基於 LLM 的驗證消除 Linux 網路堆疊中的錯誤

LLM 在尋找生產軟體中的錯誤方面已變得驚人地強大。這加劇了一個已經嚴重的風險：我們許多關鍵基礎設施是由軟體中介，而軟體中的每個錯誤都可能是潛在的漏洞。形式驗證提供了透過產生整個錯誤類別不可能存在的證明來減輕此風險的潛力，但由於它需要稀缺、昂貴的專家知識，因此實際應用有限。幸運的是，LLM 也越來越有能力進行驗證，指向一個關鍵軟體基礎設施從建構開始就安全的未來。

在這篇部落格文章中，我們報告了在 Basis 進行 LLM 引導驗證實驗的結果。我們的目標是 Linux 網路堆疊的一個關鍵元件：nftables 防火牆編譯器和最佳化器，我們打算在 Rocq 定理證明器中進行驗證。nftables 是此類關鍵基礎設施之一。它過濾幾乎每台 Linux 機器上的流量，而其中的漏洞會被視為最高嚴重性，因為防火牆若錯誤過濾，會暴露它本應保護的每一台機器。

在驗證 nftables 的過程中，我們發現了兩個關鍵錯誤，影響自 2022 年以來所有版本的 Linux（這些錯誤已向維護者揭露1）。我們的已驗證實作已被證明不含這些改變語義的錯誤，而二次實驗顯示，其中較嚴重的錯誤不會透過天真的 LLM 錯誤搜尋被發現。

我們的實驗表明，產生證明和建構穩健已驗證系統所涉及的努力正日益自動化。本文其餘部分將概述 nftables、我們發現的錯誤，以及我們使用 LLM 驗證關鍵網路軟體的過程。

nftables 及其錯誤快速入門

nftables 是 Linux 作業系統提供的防火牆機制之一。您作業系統收到的每個封包都會通過 nftables，它決定哪些封包會被轉發，哪些會被丟棄。自 2014 年取代 iptables 成為每個主要 Linux 發行版的預設封包過濾器以來，nftables 如今保護從家用路由器到容器網路的一切；如果 Linux 機器過濾流量，nftables 幾乎肯定會決定哪些能通過。防火牆是大多數網路安全層的關鍵元件，而其中的漏洞可能危及整個系統。已驗證的 nftables 實作將增加對此關鍵層的保證。

nftables 規則集與編譯管線

nftables 的完整架構如下所示，由使用者空間 CLI 工具和核心模組組成：

此 CLI 工具將使用者提供的原則序列作為輸入，以有序規則清單表示，其中每個規則匹配封包的某些部分（其來源位址、其目的連接埠、其 TCP 旗標）並傳回判定，即 accept 或 drop。例如，以下規則告訴 nftables 接受目的位址（daddr）為 192.168.50.1 或 192.168.50.2 的任何封包。

ip daddr 192.168.50.1 accept
ip daddr 192.168.50.2 accept

nft 命令列工具解析這些規則集並將它們編譯為緊湊的基於暫存器的位元組碼，然後將其載入核心。在那裡，核心的直譯器使用位元組碼為通過網路堆疊的每個封包計算判定：要麼接受它通過防火牆，要麼丟棄它。

由於此位元組碼在系統看到的每個封包上執行，它位於核心的熱路徑上，因此其效率至關重要。出於這個原因，CLI 工具還為原始碼語言提供最佳化器模組，該模組重寫您的輸入規則以更有效地執行（減少讀取次數，或移除冗餘檢查）。使用者依賴最佳化器保證的一個關鍵安全屬性是它保留輸入規則的語義。換句話說，無論封包是通過最佳化還是未最佳化的規則集，計算出的判定都應該相同。

我們開始證明 nft 命令列工具的正確性，並在此過程中發現了系統中的兩個錯誤。

發現的錯誤

我們的主要結果是發現最佳化器不產生等效程式的兩個關鍵情況：

1. 第一個錯誤是無效的最佳化，如果應用，會導致接受原本會被拒絕的封包（！！）。

2. 第二個導致最佳化器將有效規則集轉換為核心拒絕的無效規則集。

我們能夠在最新版本的 nftables 使用者空間工具中重現這些錯誤，並證明我們的已驗證重新實作完全沒有這些改變語義的錯誤。

錯誤 1：位元遮罩欄位的無效合併

第一個錯誤與合併位元遮罩欄位的最佳化有關。

封包包含一系列控制旗標位元 — 例如，TCP 封包有 SYN、ACK、FIN 等。

nftables 允許使用者編寫測試特定位元是否設定的規則：tcp flags syn 匹配任何設定了 SYN 位元的封包。因此，以下規則集會丟棄每個設定了 SYN 的封包和每個設定了 ACK 的封包：

tcp flags syn drop
tcp flags ack drop

最佳化器 nft -o 將這兩個規則合併為一個：

tcp flags { syn, ack } drop

不幸的是，此重寫是不正確的。合併後的規則不代表相同的含義。

具體來說，nft 輸入語言的語義定義為集合查詢是精確匹配測試：只有當封包的旗標位元組正好等於 syn（設定了 SYN 位元且清除所有其他位元）或正好等於 ack 時，才會丟棄封包。

原始規則問「是否設定此位元？」；合併後的規則問「旗標位元組是否正好等於此一位元，其餘全部歸零？」任何以此位元測試形式匹配的位元遮罩型欄位都會套用相同的縮小。

這個錯誤特別有害，因為它會無聲地將限制性政策轉換為更寬鬆的政策，並可能產生關鍵的安全影響：在先前的範例中，大多數 syn 和 ack 封包都會被丟棄，但最佳化後，只有只設定了 SYN 或 ACK 位元的封包會被丟棄（封包的實質較小集合）。

錯誤 2：重疊範圍的無效合併

我們發現的第二個錯誤與基於位址合併規則的最佳化有關。

當連續規則匹配相同欄位時，nft -o 會將它們合併為判定對應（vmap）— 一個將欄位值傳送到轉發判定的查詢表。這將欄位的多次讀取減少為單次讀取，然後在位元組碼中跳轉。

考慮一個丟棄一個來源位址範圍並接受另一個範圍的規則集：

ip saddr 192.168.50.1-192.168.50.123 drop
ip saddr 192.168.50.120-192.168.50.255 accept

nft -o 將兩個規則合併為：

ip saddr vmap { 
   192.168.50.1-192.168.50.123 : drop, 
   192.168.50.120-192.168.50.255 : accept 
}

不幸的是，最佳化器的實作有錯誤，產生的對應表格式不正確。具體來說，nftables 要求 vmap 必須將每個位址對應到單一判定：其鍵必須參照不重疊的區間。相反，在我們的範例中，最佳化器重複使用原始範圍而未檢查其不相交性，因此鍵在 .120–.123 重疊。因此，最佳化後，產生的規則集會被以錯誤 Error: conflicting intervals 拒絕。

此錯誤導致有效規則集被最佳化為無效規則集，使用者在嘗試安裝最佳化規則集時會收到錯誤。此案例的安全考量較不嚴重，但這仍代表不正確的最佳化，並最終降低對 nftables 的信任。

形式驗證 nftables

這兩個錯誤都是在持續驗證 nftables 使用者空間元件（即證明 nft 保留規則集的行為）的過程中，由 LLM 自主發現的。

要形式證明實作具有此屬性，我們首先必須確定規則集的含義，然後根據該含義驗證實作。

我們在 Rocq 定理證明器中形式化了四個部分：

1. nftables 規則語言的語法和語義，
2. 核心執行的基於暫存器位元組碼的語法和語義，
3. 從規則集到位元組碼的編譯器，以及
4. 將規則集重寫為更有效規則集的最佳化器。

部分 (3) 和 (4) 是我們入門中 nft CLI 工具兩個部分的已驗證對應物，而部分 (2) 扮演核心位元組碼執行器的角色。

建基於形式化語義，我們陳述並證明了編譯器和最佳化器都是語義保留的。也就是說，編譯器產生的位元組碼接受和丟棄的封包正好與輸入規則集相同，而最佳化規則集匹配的封包正好與原始規則集相同：

有兩個部分位於證明之外：將 nftables 規則集轉換為 Rocq AST 的剖析器，以及將位元組碼安裝到核心的序列化器。兩者都是未驗證的 OCaml，封裝在我們的 nftc_cli.exe 命令列工具中，該工具連結到已驗證的編譯器和最佳化器。

已驗證的實作仍在進行中，但已接近功能同等性，約 90% 的 nftables 規則語言已建模並驗證。已驗證實作中的每個定義、程式碼行和證明都是由 LLM 撰寫的。

自主驗證方法論

本節描述我們用來自動化開發的方法論。所有程式碼和證明都是由以自動模式運行的 Claude CLI 使用 Opus 4.8 模型產生的。

LLM 從指定驗證器（在本例中為 Rocq）和要驗證的 nftables 部分的詳細提示開始，並指向形式驗證和網路的先前工作。提示還說明了我們期望 LLM 遵循的證明工程和一般工程實務，例如測試驅動開發和頻繁的程式碼審查。

測試工具

我們指示 LLM 啟動使用 systemd-vmspawn 的虛擬機器（VM），並使用網路命名空間建構測試環境，在這些環境中可以安裝 nftables 規則並在不同的網路拓撲上練習。VM 還為 LLM 提供沙箱，在其中運行官方 nft 命令列工具並實驗其行為。

在此工具之上，我們執行端到端差異測試：將規則集語料庫輸入已驗證編譯器和官方 nftables 實作，並比較其輸出。

對抗工作流程

開發透過兩個 LLM 之間的對抗迴路進行：一個撰寫規格、實作和證明，另一個針對特定類型的缺陷審查它們並報告發現的內容。迴路持續進行，直到審查 LLM 確信該類型缺陷已妥善修復。

此工作流程特別有效於揭露語言語義中的保真度問題，其中實作 LLM 過早宣稱勝利，即使運算式的含義尚未精確建模（例如，將有副作用的運算式近似為純運算式）。為了揭露此類語義差距，我們將對抗模板具現化為一個審查 LLM，該 LLM 根據 nftables 的實際 C 實作交叉檢查已驗證程式碼，標記規格不足之處。

小型證明導向測試（SPOT）

為了進一步壓力測試語義，同時產生最終使用者可用於除錯其自身防火牆設定的成品，我們建構了特殊測試案例，其中 LLM 必須陳述並證明真實規則集的屬性：要麼是規則集捕捉使用者意圖的形式證明，要麼是顯示該意圖可能被違反的反例。當規則集抗拒規格和推理時，這表示語義尚不夠精確，可以改進。

錯誤是如何被發現的？

我們在這篇部落格文章中包含的兩個錯誤都是在開發過程中由 LLM 自主發現的。然而，比錯誤本身更有趣的是錯誤是如何被發現的。

重疊區間錯誤是透過測試工具發現的。6 月 30 日（69666ba），LLM 合成了大量人工規則集，旨在觸發 nftables 的最佳化器重寫並更好地理解其行為。工具在新的網路命名空間內將每個規則集通過兩個最佳化器運行並將結果載入核心。當其中一個規則集在 nft 命令列上觸發響亮失敗（conflicting intervals）時，錯誤偶然浮現。

然而，不健全位元遮罩合併錯誤的故事要精彩得多。在提交 17c949a 中，LLM 新增了其自身健全版本的位元遮罩合併最佳化。當連續規則匹配相同位元遮罩欄位時，其最佳化器將它們折疊為原始「是否設定此位元？」測試的 OR，而不是 nftables 的精確匹配集合。提交訊息顯示，LLM 已經知道集合的精確匹配語義使其不適合合併位元遮罩型運算式。然而，LLM 只使用該不健全性來證明其自身的分歧，而不是將其識別為 nftables 本身的錯誤。

事實上，根據提交訊息，LLM 試圖透過指出它正在合併的欄位（封包的連線追蹤狀態 ct state）一次最多只能設定一個位元來合理化 nftables 的錯誤合併行為。因此，合併集合 ct state { new, established }（將封包的連線追蹤狀態與 new 或 established 的精確位元進行比較）是無害的，例如可以在 Arch Linux 預設規則集 中找到。

直到我們明確提示 LLM 在 7 月 14 日的提交（c786563）中解釋其與官方最佳化器的分歧，錯誤才浮現。那時 LLM 終於意識到 nftables 的最佳化器確實會導致不健全行為，因為還有其他位元遮罩型運算式如 tcp flags 和 ct status，其中可以同時設定多個位元，並透過 VM 測試工具確認了錯誤。因此，形式驗證保護我們免受我們和 LLM 都未預期的錯誤。

在揭露這兩個錯誤後，我們進行了一個小型實驗，我們啟動新的 Claude 工作階段並指示它使用相同的 VM 測試工具在官方 nftables 最佳化器中尋找錯誤。LLM 運行數小時，成功識別出 16 個錯誤，其中 3 個涉及無聲改變語義，13 個涉及因無效最佳化規則導致最佳化器當機。我們正在向維護者揭露這些錯誤。

# original ruleset
ip daddr 1.1.1.0/24 
     ip daddr 1.1.1.5 accept
ip daddr 2.2.2.0/24
     ip daddr 2.2.2.5 accept

# after nft -o
ip daddr 1.1.1.0/24
   ip daddr { 
     1.1.1.5, 2.2.2.5
   } accept
# 2.2.2.5 can never match

Claude 是否成功找到我們驗證工作中浮現的兩個錯誤？答案是否定的！雖然重疊區間錯誤確實被 Claude 發現，但位元遮罩錯誤在運行數小時後仍未被發現。事實上，從檢查聊天記錄來看，即使我們運行更長時間，LLM 也不太可能發現該錯誤，因為它成功重現了能夠觸發最佳化器錯誤的精確規則集，但認為新的輸出合理並決定繼續前進。與 LLM 確實透過目視檢查錯誤輸出規則發現的 3 個無聲錯誤不同，位元遮罩錯誤需要更深入理解 nftables 語義的含義。

最後，一個或許更令人鼓舞的結果是，已驗證實作不易受到 Claude 發現的 3 個最佳化錯誤的影響。儘管已驗證實作仍在進行中，LLM 產生的語義捕捉了足夠多的 nftables 以透過正確性定理拒絕那些錯誤的最佳化規則。更聰明的模型可能更擅長識別錯誤，但形式驗證確實為我們提供了更高層級的保證。

發現與觀察

在這次初步驗證努力的過程中，大部分人力投入在驗證、審查和精煉規格上。雖然失敗的證明很容易消除，因為 LLM 會持續工作直到 Rocq 接受，但可能輕易錯過被悄悄弱化的定理。

對於它不想做的工作，我們經常發現 LLM 會以某種方式縮小任務，而隨意閱讀可能輕易錯過。

我們看到這種情況有兩種反覆出現的形式：

1. LLM 以方便的前提條件弱化其規格，以及
2. LLM 扭曲系統設計以使困難的引理永遠不會出現。

以前提條件弱化定理

最佳化器的正確性定理提供了此失敗模式的代表性範例。

最佳化器實作的一部分需要產生新鮮名稱，這通常意味著在周圍程式碼中穿線名稱產生狀態。

這些名稱僅在重寫具有副作用的規則（更新狀態或修改封包的規則）時需要。LLM 沒有進行配管，而是縮小了其定理必須說明的內容：

Theorem optimize_table_correct :
  forall n d c n' d' c' base p,
    optimize_table n d c = (n', d', c') ->
    rules_clean (c_rules c) = true ->
    … ->
    eval_chain c' (set_env p (env_with_sets base d'))
  = eval_chain c  (set_env p (env_with_sets base d)).

具體來說，被微妙插入的 rules_clean 假設是一個僅對純規則成立的述詞。有了這個限制，定理可以在沒有配管基礎設施的情況下被證明。定理仍被命名為 optimize_table_correct 並被證明正確，儘管陳述現在對具有副作用的規則沒有說明。

剖析器中的暫存器配置

有時 LLM 會透過重塑規格定義本身而非直接重塑定理來捷徑。一個這樣的範例出現在暫存器配置實作中：nft 編譯器針對核心的基於暫存器位元組碼直譯器，因此在編譯管線的某個點上，編譯器必須配置暫存器。

LLM 試圖透過將暫存器延伸到來源 AST，讓剖析器（位於已驗證核心之外）指派它們來避免證明有關暫存器配置的引理。

這導致了一個難以理解的設計，其中部分配置在剖析期間發生，但就 LLM 的證明義務而言，編譯器變得更容易驗證，因為複雜邏輯被外包給未驗證的程式碼。

結論

驗證並非新事物。數十年來，研究人員投入大量人力驗證關鍵軟體基礎設施，並在此過程中經常發現關鍵錯誤。新的是，這項人力現在正透過 LLM 的使用日益自動化。雖然仍在進行中，即使是我們在這個專案上的中期進展，也可能需要數年的人力才能完成；在 LLM 的助力下，我們在數週內達到可運作的實作。我們獲得與傳統驗證相同的益處：我們正朝著內建正確性證明的重新實作邁進，並在此過程中發現 nftables 最佳化器中的關鍵錯誤。

然而，部分人力仍需手動進行。LLM 反覆試圖縮小其任務範圍並拖延具有挑戰性的證明。我們開發中的大部分人力投入在捕捉此行為。是否能透過更複雜的工具或模型能力的進步來自動化這最後一步，仍有待觀察。

我們打算親自找出答案。我們的下一個目標是完全自動化的管線，能夠在沒有人類介入的情況下大規模驗證關鍵軟體基礎設施。