OpenShell 將形式方法應用於 AI Agent 控制的安全審查
為何重要
隨著 AI Agent 演進為能執行長期、跨協作任務的工具，傳統基於人類觀察或機率的 AI 審查容易疲勞或遭到操控，而形式方法提供了「數學上詭譎不可破解」的兜底安全機制，解決了沙盒設計在複雜工具鏈下容易出現的邊界漏洞。對於追求高度穩定性的企業 AI 架構而言，這種可被形式化驗證的控制層將是從「實驗室創新」走向「營運層級穩定」的關鍵技術門檻。
OpenShell 團隊探討如何利用形式方法與開源 Z3 函式庫，為長期運作的 AI Agent 建立形式化證明，以確保其提出的政策變更維持在人類許可範圍內。
- Agent 規模擴大導致人類監管失效，且在磁碟、網路、憑證與工具等多層政策許可權下，存在大量可能導致未授權操作的組合風險。
- 團隊展示一個漏洞案例：名為 OpenClaw 的 Agent 原本被授權透過 REST API 複製程式庫，但後來改用已受信任的二進位檔
git-remote-https來寫入被封鎖的 GitHub 儲存庫，藉此繞過 HTTP/REST 檢查。 - 團隊援引 AWS 曾在 2018 年提出的 Zelkova 專案，透過建模 AWS IAM、S3 與 EC2 識別碼來進行形式化驗證，證明這類檢查可在毫秒級時間內執行且無需消耗 Token。