AWS 以 33 萬行 Isabelle/HOL 機器驗證，為 EC2 虛擬機器隔離提供數學保證
Amazon Science · 2026-06-12
AWS 於 2026 年 6 月 12 日公開宣布，EC2 Nitro 隔離引擎（Nitro Isolation Engine）已完成形式驗證，成為全球首個部署於商業雲端環境的形式化驗證 Hypervisor。驗證工作由 AWS 研究員 Dominic Mulligan 主導，共產出約 330,000 行以 AutoCorrode 函式庫輔助、在 Isabelle/HOL 中完成的機器驗證證明，涵蓋執行於 AWS Graviton5 EC2 執行個體的 Rust 可信計算基礎（TCB）。
背景
傳統雲端安全依賴程式碼審查、模糊測試與滲透測試，但這些方法本質上無法窮舉所有執行路徑。Nitro Hypervisor 自 2017 年隨 AWS Nitro 系統推出後，一直是 EC2 VM 隔離的核心元件，負責仲裁所有虛擬機器對記憶體、CPU 暫存器狀態與 I/O 裝置的存取。隨著 Graviton5 世代到來，AWS 選擇對這個最小化可信計算基礎進行形式驗證，將安全保證從「測試覆蓋率」推進至「數學正確性」。
Nitro Isolation Engine 以 Rust 撰寫，採用極小介面設計：所有 VM 互動均透過一組嚴格定義的 API 進行。這種最小化設計是形式驗證得以實施的前提，可驗證的程式碼面積越小，proof obligation 越易管理。AutoCorrode 是 AWS 於 2025 年開源的 Isabelle/HOL 驗證基礎設施，包含 μRust 語言形式化、基於分離邏輯（Separation Logic）的規格語言，以及利用最弱前置條件演算（weakest-precondition calculus）的自動證明策略 Crush。
核心改動
驗證工作確立了三類性質。第一是功能正確性：涵蓋 VM 建立、記憶體映射與中止處理等所有操作，數學上保證記憶體安全、終止性與執行期錯誤不存在。第二是機密性：以非干擾（noninterference）風格的性質，證明客體 VM 狀態對系統動作的任意觀察者均不可見。第三是完整性：在不同 VM 上執行的操作，無法影響其他 VM 的私有狀態。
方法論上，研究團隊為 Rust 核心子集建立了形式語意 μRust，以分離邏輯撰寫各函式的前置／後置條件規格，再透過 Crush 策略族與 Autogen（自動推導 record 操作交換律的工具）驅動 Isabelle/HOL 完成機器驗證。整個驗證流程不依賴任何人工繞過，所有 330,000 行證明均可在 Isabelle/HOL 中重現執行，此技術細節由劍橋大學電腦科學系 Mulligan 於 2026 年 2 月的 Logic and Semantics Seminar 中完整報告。
影響範圍
此驗證成果已部署於 M9g 與 M9gd 執行個體（基於 Graviton5），自 2026 年 6 月 10 日起正式上線。對 EC2 用戶而言，不需任何操作變更，現有工作負載即可受惠於數學級別的隔離保證。對整個雲端產業而言，這是形式驗證技術首次在生產規模 Hypervisor 落地，打破了「形式驗證只適用於小型學術系統」的既有認知。
- 驗證工具鏈：Isabelle/HOL +
AutoCorrode（μRust、Separation Logic、weakest-precondition calculus） - 機器驗證規模：約 330,000 行 HOL 證明
- 部署平台：AWS Graviton5 EC2（
M9g／M9gd執行個體） - 驗證性質：功能正確性、機密性（noninterference）、完整性
Dapr 1.18 引入可驗證執行：以密碼學簽章鏈讓工作流程歷程無法偽造
CNCF Blog · 2026-06-11
CNCF 於 2026 年 6 月 10 日發布 Dapr v1.18.0，核心新能力為「可驗證執行」（Verifiable Execution）：透過 SPIFFE X.509 身分與密碼學簽章鏈，使工作流程的執行歷程具備防竄改與可獨立驗證的特性。這項功能瞄準分散式系統與 AI 代理場景，讓「可觀測性告訴你發生了什麼」升級為「可驗證性讓你能夠證明它」。
背景
Dapr 工作流程引擎長期以 actor 狀態儲存記錄每個執行步驟，但這些歷程記錄不帶任何密碼學保護，任何具有狀態存儲寫入權限的角色均可在不留痕跡的情況下竄改。隨著金融、醫療與製藥等受監管行業將核心業務邏輯遷移至 Dapr，以及 AI 代理系統大量委派工作給其他服務，「這個請求究竟是哪個工作流程發出的」成為合規與安全的關鍵問題。
Dapr 既有的 mTLS 工作負載身分基礎建立於 SPIFFE 規範之上，每個 sidecar 均持有格式為 spiffe://<trust-domain>/ns/<namespace>/<app-id> 的 X.509 SVID。v1.18.0 以此為信任錨點，將工作流程執行的每一步驟與 sidecar 的私密金鑰綁定，形成可驗證的執行鏈。
核心改動
工作流程歷程簽章（Workflow History Signing）是最基礎的一層：每批次歷程事件先以 protobuf deterministic 模式序列化，再計算 SHA-256 摘要，並以 SHA-256(previousSignatureDigest || eventsDigest) 的方式串連前一筆簽章，最後以 sidecar 的 SPIFFE X.509 私密金鑰（支援 Ed25519、ECDSA P-256、RSA）完成簽署。驗證時需逐一核查鏈結完整性、事件連續性、摘要重算、憑證時效、Sentry CA 信任鏈，以及 SPIFFE ID 是否符合工作流程所屬應用程式。
跨應用程式邊界的保護由 ChildCompletionAttestation 與 ActivityCompletionAttestation 兩種結構承擔：執行者在回報完成時，必須簽署包含父工作流程 ID、任務排程 ID、輸入／輸出 SHA-256 摘要與簽署者憑證摘要的 attestation，父工作流程在接受完成事件前會驗證這些 attestation。工作流程歷程傳播（Workflow History Propagation）則提供 Lineage（完整祖先鏈）與 OwnHistory 兩種模式，讓子工作流程可取得上游執行脈絡。
apiVersion: dapr.io/v1alpha1
kind: Configuration
metadata:
name: my-config
spec:
features:
- name: WorkflowHistorySigning
enabled: true此版本同步推出 WorkflowAccessPolicy CRD，提供純允許清單的存取控制，指定哪些 appID 可呼叫哪些工作流程與活動。Jobs API 晉升為穩定版、HotReload 預設啟用，以及新增 MCPServer 資源（將 Model Context Protocol 工具呼叫封裝為持久工作流程）也同步上線。
影響範圍
啟用簽章後有一個不可逆承諾：一旦工作流程以簽章模式建立，就必須永遠執行在啟用簽章的主機上，無法回頭。預設自簽根 CA 的效期為一年，官方文件強烈建議在 CA 到期前選擇三種策略之一：保留同一根金鑰輪換葉憑證（推薦）、自帶 CA 並控制根金鑰儲存，或在切換新根前排空所有已簽署工作流程。CA 效期規劃是採用此功能最重要的運維前置工作。
對 AI 代理場景而言，可驗證執行提供了一種新的信任模型：下游服務可根據已驗證的執行來源（而非假設）做出決策。搭配同版本新增的 MCPServer 資源，Dapr 開始將可驗證性延伸至 LLM 工具呼叫鏈，為代理委派模式提供密碼學級別的審計基礎。
- 簽章演算法：
Ed25519、ECDSA P-256、RSA（由 mTLS 設定決定） - 鏈結機制：
SHA-256(previousSignatureDigest || eventsDigest) - 竄改偵測錯誤碼：
DAPR_WORKFLOW_HISTORY_TAMPERED - 狀態儲存 key 前綴：
history-NNNNNN、signature-NNNNNN、sigcert-NNNNNN - 根 CA 預設效期：一年（需提前規劃輪換策略）
Docker Hardened Images 整合 Aikido 掃描：VEX 聲明自動過濾假陽性 CVE
Docker Blog · 2026-06-11
Docker 與資安平台 Aikido 於 2026 年 6 月 11 日宣布整合：Aikido 掃描器現已原生支援 Docker Hardened Images（DHI）並讀取隨映像發布的 OpenVEX 聲明，將 Docker 已確認不可利用的 CVE 自動從待處理佇列中移除，同時保留完整稽核軌跡。這是容器供應鏈安全領域「掃描器直接消費映像發布者 VEX 資料」的首個主要商業整合案例。
原本的問題
現代容器映像掃描面臨兩個結構性困境。其一是 CVE 體積：AI 編碼代理快速組裝軟體、拉入數百個依賴，導致一張通用基礎映像動輒回報數百筆 CVE，多數為無法實際利用的假陽性。其二是 distroless 映像破壞傳統掃描工具：缺少套件管理員與 shell 的映像讓依賴路徑分析失效，使誤報率進一步上升。結果是安全團隊將大量時間花在分類注定無法修補、或根本不存在風險的發現。
DHI 的設計在技術上已提供解決基礎：映像隨附以 SPDX 2.3 格式簽署的 SBOM，透過 OCI 1.1 referrer lookup 或映像內 /opt/docker/sbom/ 路徑發布，並附上 OpenVEX 聲明標示每筆 CVE 的可利用狀態。DHI 亦達到 SLSA Build Level 3 出處認證，並提供 17 種以上的供應鏈 attestation。問題在於，過去需要人工將這些資料餵入掃描流程。
採用的方法
Aikido 整合後，掃描流程分為四個自動化步驟：偵測（從映像參考與 Docker Hub registry metadata 識別 DHI 基礎映像）、目錄建立（拉取隨映像簽署發布的 SPDX 2.3 SBOM）、比對（以 PURL 對 Docker OSV feed 與上游 advisory feed 進行元件比對），最後套用 VEX（疊加 Docker 發布的 OpenVEX 聲明，壓制標記為已解決的發現）。此流程不需額外設定，Aikido 在連接 Docker Hub 後自動偵測硬化映像並執行。
| VEX 狀態 | 含義 | Aikido 行為 |
|---|---|---|
Fixed | 此映像已修補該漏洞 | 標記為已修復 |
Not Affected | Docker 確認不可利用或為假陽性 | 自動壓制，保留稽核記錄 |
Under Investigation | 影響仍在評估中 | 保留在佇列中 |
Affected | 漏洞適用，尚無修補 | 顯示為待處理 |
實際效果
以一個常見場景為例：某個解析器函式庫 CVE 在多數基礎映像中都會觸發，但在 DHI 建置中，該漏洞的可利用程式碼路徑並不存在。Docker 在該映像的 OpenVEX 聲明中標記 not_affected，Aikido 讀取後將此 CVE 從主動審查佇列中移除，開發團隊完全不會在每日待辦清單中看到這筆項目，但稽核員仍可在完整記錄中找到它及其排除理由，符合 SOC 2、FedRAMP 等合規需求。
就量化效果而言，一般通用基礎映像掃描回傳「數百筆 CVE」的情況，在套用 VEX 後可縮減至「少數幾筆真正需要處理的發現」。這個整合確立了一個模式：映像發布者可透過標準化 VEX 資料主動降低下游掃描噪音，而非讓每個掃描工具各自猜測可利用性，供應鏈安全的責任從掃描器移向更有能力做出判斷的映像維護者。