Static Analysis for Zero-Knowledge Programming Languages, Filipe Casal - DeFi Security Summit 2022
三句話摘要
介紹零知識編程語言的靜態分析工具，防止加密應用中的代碼漏洞。 靜態分析工具對新興零知識編程語言而言必不可少，能有效防止設計缺陷導致的安全漏洞。 零知識證明的核心優勢在於可擴展性——應用方只需驗證證明而不必重新計算整個程序，使其成為處理大規模計算的高效解決方案。
重點整理
重點- 1
零知識證明的核心優勢在於可擴展性——應用方只需驗證證明而不必重新計算整個程序，使其成為處理大規模計算的高效解決方案。
- 2
零知識編程語言仍處於發展初期，語言設計存在缺陷且開發者工具極為有限，主要導致開發和測試困難，容易產生難以察覺的漏洞。
- 3
Amarna 靜態分析器已實現 14 個檢測器用於 Cairo，包括捕捉隱式函數導入等對傳統編程語言使用者不明顯的錯誤。
- 4
Circumspect 靜態分析器用於 Circum 語言，採用 SSA 中間表示進行數據流分析，可檢測約束執行中的未使用變數等問題。
實用技巧與重點
乾貨- Amarna 工具：14 個檢測器（第 12 個為隱式函數導入檢測）、支援 pip 安裝、可輸出 Sarif 格式、提供 GitHub Action 整合、計畫開發 VS Code 原生擴充
- Circumspect 工具：約 6-7 個檢測器、預計未來數週發布、用 Rust 開發、計畫加入 SSA 和數據流分析、支援 Sarif 格式輸出
- 實際漏洞案例：Tornado Cash 使用錯誤的賦值運算子（`=` 而非 `<=`）導致約束未強制執行，允許偽造證明竊取資金
- 應用案例：YDX 由 Cairo 驅動、Tornado Cash 由 Circum 驅動，皆涉及數百萬美元資金
- Circum 使用建議：編譯時加入 `--inspect` 標誌以捕捉編譯器未發現的問題
結論
結論“靜態分析工具對新興零知識編程語言而言必不可少，能有效防止設計缺陷導致的安全漏洞。”
完整解析
詳細演講者 Flip 來自密碼學研究公司 Trailbeats，致力於軟體安全研發。他介紹了零知識證明（ZKP）的基本概念：一個人可以證明自己知道某個秘密輸入會使程序產生特定輸出，而驗證方無需重新執行程序即可確認該證明的真實性。這種特性使零知識證明在需要驗證大規模計算的應用中具有顯著優勢，成為區塊鏈等領域的關鍵技術。
要生成零知識證明，開發者需將程序編碼為數學約束和多項式形式，因此出現了零知識編程語言如 Cairo 和 Circum。然而，這些語言仍是新興技術，存在大量設計缺陷，開發者工具匱乏（基本只有語法高亮），使開發、測試和審計極其困難。由於涉及資金龐大的應用如 YDX（Cairo）和 Tornado Cash（Circum），漏洞的後果極為嚴重。
為此，Trailbeats 團隊開發了 Amarna——Cairo 的靜態分析工具，已實現 14 個檢測器，能捕捉傳統編程語言使用者容易忽視的問題。例如，Cairo 的 import 語句會隱含導入帶 `@test` 裝飾器的函數，使其在合約中被意外暴露。Amarna 可透過 pip 安裝使用，支援 Sarif 格式輸出與 GitHub Action 整合，未來將推出 VS Code 原生擴充。
同時，Circumspect 工具正在開發中，用於分析 Circum（一種更底層的電路編譯器語言）。該工具使用 Rust 編寫，利用已有的 SSA 中間表示進行數據流分析，可檢測約束執行中的未使用變數。這類問題在 Tornado Cash 的實際漏洞中出現過——開發者誤用賦值運算子導致約束未被強制執行，允許攻擊者偽造證明。Circumspect 預計於未來數週內正式發布，同樣支援 Sarif 與 GitHub 整合。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
