Statically Safe: Proving Security with Semantic Queries
三句話摘要
利用精確靜態分析查詢，讓審計人員能從待辦清單中劃掉已排除的漏洞，從根本降低代碼審計的認知負荷。 靜態分析的最大價值不在於發現更多問題，而在於能可信地確認「某類漏洞不存在」，讓審計員安心地從追蹤清單中移除項目。 認知負荷隨漏洞可能性指數增長：審計時每發現一個潛在問題，需檢查的調用點與場景隨之倍增，將創造性漏洞挖掘變成容易出錯的機械勞動。
重點整理
重點- 1
認知負荷隨漏洞可能性指數增長：審計時每發現一個潛在問題，需檢查的調用點與場景隨之倍增，將創造性漏洞挖掘變成容易出錯的機械勞動。
- 2
工具必須能給出可信的「否」：目前多數工具著重「告訴你有問題」，但審計人員更需要的是「確認這個問題不存在」，才能從內部追蹤迴圈中移除該項目。
- 3
靜態分析應支援自定義查詢而非只有內建檢測器：能用類 SQL 語言精確描述「我要找什麼」與「我要排除什麼」，才能針對具體協議的特定風險提問。
- 4
精確語言是建立信任的基礎：Dijkstra 的觀點——自然語言不足以處理立法、數學或程式設計中的複雜情況；同理，模糊的描述無法支撐可信的安全結論。
實用技巧與重點
乾貨- 審計關注的漏洞類型舉例：提款前是否執行健康檢查、地址是否已通過白名單驗證、重入攻擊風險
- 被比較的技術方案：AI 輔助、模糊測試（fuzzing）、正式驗證（formal verification）、靜態分析（static analysis）
- 工具設計的三個評估維度：可自定義查詢、自動檢測（不增加手工量）、結果可信（無誤報）
- 靜態分析語言風格：類 SQL 查詢語言（講者來自 Audit Central 的案例）
- 核心使用場景：找出「是否每次提取前都做健康檢查」、「某地址是否在調用鏈某處已被驗證」
結論
結論“靜態分析的最大價值不在於發現更多問題，而在於能可信地確認「某類漏洞不存在」，讓審計員安心地從追蹤清單中移除項目。”
完整解析
詳細代碼審計最令人疲憊的不是找到漏洞本身，而是在審計過程中持續追蹤越來越多「潛在攻擊路徑」所產生的認知負荷。講者以貸款協議為例：審計員需要確認提款前是否總是執行健康檢查、某個地址是否在調用鏈的某個環節已被驗證不會導致重入攻擊。問題在於，這類確認不是一次性的——每個函數、每個調用點都需要獨立追蹤，需要的謹慎程度遠超過實際找到漏洞的數量，最終讓富有創造性的漏洞挖掘工作退化為壓力極大、易出錯的機械式記錄。
面對這個問題，業界已有多種技術方案：AI 輔助分析、模糊測試、正式驗證、靜態分析。講者將這些方案對照三個維度進行評估——能否提出自定義查詢、是否真正自動化（不是把工作轉移給使用者）、結果是否可信（無誤報）。他指出，目前多數靜態分析器的主要設計模式是「內建檢測器」，無法讓審計員針對自己具體的疑問提問；而正式驗證雖然嚴謹，但等同於將大量工作（定理證明）轉移到審計員身上。
講者認為最關鍵的缺口在於：工具必須能夠可信地回答「不，這個漏洞不存在」。只有當工具能給出這個答案，且審計員可以相信它沒有誤報時，才能真正從審計待辦清單中劃掉某個項目，不再需要在每個調用點重複追蹤。他提出的解法是以不同於現有使用方式的角度運用靜態分析器——透過類 SQL 的查詢語言，讓審計員精確描述「我要在代碼庫中找到什麼」以及「我要排除什麼」。
引用 Dijkstra 的觀點作為收尾：自然語言對於複雜精確的情境（立法、數學、程式設計）遠遠不夠用。同理，只有能夠精確表達查詢意圖的工具，才能提供可信的結論，從而真正降低審計的認知負荷，讓安全審計回歸到有創造性的工作本質。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
