RTL Anti-Tampering Design 第十六課：設計審查與證據包

安全結論要能回答：保護什麼、假設哪些故障、哪些邊界已驗、哪些反例仍成立，以及未知項在哪裡。證據包的目的不是堆報表，而是讓另一位工程師能重跑並指出結論邊界。

第十六課：設計審查與證據包

從 claim 到 evidence

建築驗收不能只交一張「合格」貼紙；要知道檢查的是哪一層、哪個日期、哪些房間未開放。硬體安全審查也從可反駁 claim 開始，例如「在最多一個保存旗標 transient upset，且 checker / clock / reset / 接受端可信時，任何未授權交易不會 commit」。生活類比不取代產品威脅模型或評估認證。

claim 需列資產與接受邊界、attacker能力、fault target/effect/timing/budget、trusted components、環境、design revision與排除項。每項證據標成 requirement、RTL review、simulation、formal、netlist、physical measurement 或 product test；不同等級不可互相代替。

coverage 不只是一個百分比：列 target × effect × time × lifecycle × reset/domain bins 的分母與空格；列 fault-free/authorized controls、反例與重播 hash。將每個反例連到根因、修補提交、重新驗證結果。工具 unsupported 或無法觀察的項目列為 unknown，不放到 covered。

審查結論分「在範圍內未找到反例」「存在反例」「證據缺失」「假設無法驗證」。第一種不代表零風險。產品 release 要由責任人接受 residual risk，不能由模型摘要自動替代。

讓審查可以重現

包內放 claim ID、版本與來源、工具/命令、輸入與 seed、hash、分類規則、coverage matrix、失敗 trace、限制、未知項目、負責人與日期。讓審查者先從 claim 挑一條最可能推翻結論的路徑，再各重播一筆 counterexample 與控制案例。

離線互動實驗

RTL／SVA 審查方向

以下為性質草案：先定義 harness 的 transaction、reset 與 oracle，並確認取樣邊界，再接入設計；尚未編譯或證明。

assert property (@(posedge clk) disable iff (!rst_n)
  accepted_commit |-> reference_authorized);

cover property (@(posedge clk) disable iff (!rst_n)
  accepted_commit && reference_authorized);

若 accepted_commit 從未成立，這個 implication 仍可能因前件不成立而 vacuous pass。用 cover 確認合法接受路徑可達。這不代表故障路徑一定可用；另要記錄因未觸發而失去可用性的情況。

此片段不證明 CDC、timing、side-channel 或實體注入；需由各自工具與測量提供證據。

檢核問題

辨認：security claim 與 supporting evidence 有何不同？ 推理： Claim 說明在指定假設下應成立的事；Evidence 記錄用來評估它的 artifact、方法、輸入與觀察結果。
比較：獨立 test oracle 與晶片防護有何不同？ 推理： Oracle 提供 testbench 預期結果，不會阻止 DUT 接受未授權操作。
情境：reviewer 只收到 counterexample 截圖，沒有 seed 或 input trace，能重播嗎？ 推理： 無法可靠重播。需提供 source/DUT hash、工具與版本、設定、seed、輸入、預期結果及 replay command。
故障診斷：報告寫 coverage 95%，卻沒有分母或未觸及 bins，還缺什麼？ 推理： Review 無法判斷涵蓋哪些 target/time 案例，也不清楚百分比的分母。應列完整分母與空 bins。
設計風險／轉移：physical validation 不在本次 campaign 範圍，release packet 要如何呈現？ 推理： 明列為 open unknown，說明影響、負責人與所需證據。不能把未完成資料包寫成產品保證。

延伸閱讀

NIST SP 800-193

MY ACADEMY · LESSON FILM

教學影片

影片依序說明本課的資料路徑。看完一段，可以回到下面的互動練習，改變輸入或故障條件。動畫呈現教學模型；它沒有替代 RTL 模擬。

圖卡的範圍說明
教學模型 · 非 RTL 模擬或晶片實測
可重播證據只支持所列範圍；不代替產品驗證、認證或風險接受

下載 MP4 · 字幕 VTT

旁白使用合成聲音。互動教學與動畫均有模型邊界；請以本課的來源與驗證範圍解讀結果。

Wrap-up｜把這一課帶回設計審查

威脅模型與成立條件: Claim 限定資產、接受邊界、故障能力、信任元件、版本與排除項。
失效原因: 用單一通過率、工具 PASS 或沒有反例推論全面安全，忽略覆蓋空格與未驗假設。
防護方法: 逐 claim 連接可重播 evidence、coverage 分母、失敗 trace、修補與殘餘風險接受者。
驗證方式與待做檢查: 檢查版本/hash/命令/seed/coverage bins/控制組/反例/限制/未知項；資料包可由另一人抽樣重播。
防護界線與未驗證項目: 文件與模型證據只支持所列範圍，未取代產品驗證、認證範圍或風險決策。

換個情境再想一次

選一個 CDC 未驗假設，補上可接受的最小證據與 owner；哪些缺口必須阻止 release？

以上整理對照本課的教學案例、參考資料與實驗範圍；未列為已完成的驗證，都是後續工作。