針對 ISA 合約驗證 RTL 處理器的模組化方法
為何重要
這項研究為硬體信任區塊 (HTB) 和隱私計算提供形式化的理論基礎，解決了硬體效能最佳化常伴隨的安全性風險。對於 RISC-V 這類開放架構而言，建立這類從抽象層次規範硬體行為的新標準，將影響未來 IP 授權安全評估與 EDA 工具鏈的發展方向。
研究團隊提出一種名為 Granite 的模組化驗證方法，旨在確保硬體元件（RTL）在功能正確性與安全合約（ISA contracts）下的非洩漏特性。該論文由 MIT、Google 和華盛頓大學共同釋出，試圖從理論層面證明流水線 RISC 設計的特性僅取決於 ISA 洩漏合約中的控制專案。
- 論文標題為「Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts」，發表於 2026 年 7 月。
- 研究證實，帶有預測機制、精確中斷和 I/O 的流水線 RISC 設計，其週期級 timing 僅由 ISA 洩漏合約中定義的「可觀測值」(observables) 決定。
- 若程式符合「金鑰密碼學常數時間」等規範（即 keep observables independent of secrets），則此方法證立其完全不受制於已知或未知時序側通道的資訊洩漏。