Meta用從不執行程式的靜態分析器在投產程式碼中發現了10萬個缺陷
Meta的Infer利用抽象詮釋和雙向推理，透過推理程式碼結構而非執行來發現空指標解引用、記憶體洩漏和競態條件。以下是它的運作原理以及如何在您自己的程式碼庫中使用它。
Meta已經發布了超過10萬個由靜態分析器在程式碼到達使用者之前捕獲的缺陷修復。這個工具名為Infer，它是開源的，並且不會執行您的程式碼。它讀取程式碼，建構程式碼可能執行的數學模型，並證明某些壞事不可能發生。或者它會找到一條可能發生的路徑。…
想法與洞見
探索 AI 優先開發、編碼護欄和可處置架構。
靜態分析無法證明你的飛機不會墜毀，但它能證明更有價值的事
抽象解釋會對每一個可能的程式狀態進行過度近似。如果除零錯誤在抽象層中無法觸及，那麼在真實程式碼中也同樣無法觸及。以下是它的運作原理與局限性。
靜態分析無法證明飛機不會墜毀。但它可以證明你的高度計控制迴路絕不會發生除零、絕不會陣列索引越界，也絕不會讓定點累加器溢位。這兩者之間的區別至關重要：前者是關於物理、空氣動力學，以及鋁合金在壓力下的主張；後者則是關於你可以在飛機離地前就驗證完的程式碼。…
如何證明你的程式沒有執行時錯誤（以及為什麼你很可能會放棄嘗試）
抽象解釋讓你在執行前就能證明執行時錯誤不可能發生。以下說明它實際上如何運作、為什麼很困難，以及它在你的工具鏈中扮演什麼角色。
你的測試套件通過了。你的型別檢查器是綠燈。你發布了。兩小時後，生產環境在某個沒人想到要測試的邊緣案例上拋出了 。 測試能找到錯誤。型別能防止一部分。但兩者都無法證明你的程式完全沒有執行時錯誤。為此，你需要更強大的東西：一種能夠同時對所有可能的執行路徑進行推理、而不需要實際執行程式的方法。…
你的 C 程式碼可以在 capability 硬體上執行，而且不需要全面 rewrite
CHERI 的 hybrid ABI 讓你逐步將 C 程式碼移植到 capability 硬體上。以下介紹如何編譯、會遇到什麼問題，以及如何在不 rewrite 整個 codebase 的情況下修復它們。
你手上有一份龐大到無法用 Rust rewrite、卻又關鍵到不能放任緩衝區溢位風險的 C codebase。CHERI capability 硬體承諾在 CPU 層級攔截記憶體安全違規，但網路上不斷有人告訴你 CHERI 指標是 128 位元，而你的程式碼假設它是 64 位元。 好消息是，CHERI…
Capability 硬體沒有失敗，它只是早了四十年
硬體層級的記憶體安全性自 1970 年代就已可行。以下是 capability 架構為何一再敗給扁平記憶體模型，以及 CHERI 為何終於改變了這道算式。
七成 CVE 是記憶體安全性錯誤。buffer overflow、釋放後使用、重複釋放。這類漏洞讓攻擊者得以從一張損毀的 JPEG 取得 root 權限。 我們自 1975 年起就知道如何在硬體層面阻止絕大多數這類問題。劍橋 CAP 電腦採用了 capability 定址。卡內基美隆大學的 Hydra…
你的 C 相依程式庫可能讓整個行程當掉。WebAssembly 可以阻止它。
用 container 來隔離單一 C 程式庫未免小題大做。將其編譯為 WebAssembly，在 WASI sandbox中執行，即可實現記憶體安全、基於權能的檔案系統存取和當機隔離，無需 Docker。
C 程式庫內部的一次空指標解參照就可能導致整個應用程式當掉。如果該程式庫負責剖析使用者輸入、解壓縮影像或處理網路 protocol，那麼一個格式錯誤的封包就足以引發當機。container 確實能解決這個問題，但僅為了一個相依項目就啟動 Docker，無異於為盆栽雇用保鏢。你需要的是沒有額外負擔的隔離。…
你的手機已經擁有能偵測記憶體損壞的硬體
ARM Memory Tagging Extension 和 GWP-ASan 讓現代行動裝置在生產環境中偵測記憶體安全成為可能。本文介紹它們的工作原理和權衡取捨。
你的手機可以在生產環境中偵測記憶體損壞。不是用你在 CI 中執行的完整插樁，也不是針對每一次分配。但你口袋裡的硬體在幾年前就已經搭載了必要的原語，而且越來越多的生產應用正在悄悄啟用它們。 簡而言之：AddressSanitizer 對生產環境來說太貴了。ARM Memory Tagging Extension…
buffer overflow之所以反覆發生，是因為我們在軟體層面修復它
CHERI是一種硬體擴展，它將每個指標轉變為帶有邊界的權能。本文介紹它如何在CPU層面阻止buffer overflow、代價幾何，以及如何在真實硬體上試用。
buffer overflow在CWE Top 25榜單上盤踞了二十年之久。我們擁有堆疊金絲雀、ASLR、DEP、控制流完整性以及記憶體安全語言，然而它們仍然不斷出現在關鍵程式碼中。原因很簡單：這些緩解措施無一不是在軟體中執行的，而軟體可以被繞過、被錯誤配置，或者根本未被啟用。…
LLM 無法證明你的程式碼正確，但它能撰寫那些繁瑣的輔助程式
Cleanroom 驗證需要生成並消除證明義務（proof obligations）。以下說明 LLM 如何自動化註解與驗證條件（VC）的生成，讓你能專注於真正困難的證明工作。
Cleanroom 軟體工程要求你在編譯程式碼之前，先證明它是正確的。這聽起來很高尚，直到你花了三個小時為一個只排序十個整數的函式撰寫迴圈不變式（loop invariant）為止。 瓶頸不在證明本身，而在於那些繁瑣的樣板程式碼。生成驗證條件（verification…
Cleanroom 達到每千行 0.1 個缺陷。你不需要全盤照搬也能達到這個目標。
Cleanroom software engineering 將 defect rate 降低 100 倍，但全面採用需要獨立的 test team 和 formal proof。這裡介紹一種 pragmatic subset，無需 overhead 即可捕獲大部分收益。
Cleanroom software engineering 每千行程式碼僅產生 0.1 個缺陷。業界平均水準是 10 到 50。問題是，完整的 Cleanroom 要求你將團隊拆分為 author 和 verifier，在每個 module 之前編寫 formal specification，並禁止…