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

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

學習目標與課堂安排

完成本課後，你應能：

將 claim、接受邊界、方法、責任及狀態填成可審查證據表。
重播反例與合法控制，拒絕沒有分母的通過結論。
辨認 coverage 投影損失，準備保留未知項的風險紀錄。

建議 50 分鐘的教師安排：claim 定義 10 分鐘、反例重播 15 分鐘、分母與維度演算 15 分鐘、風險紀錄討論 10 分鐘。時間含學生手算、互動與討論；這是教學規劃，尚未做學生課堂時間量測。

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

從 claim 到 evidence

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

每項安全陳述（claim）都要附上以下條件，讓審查者能判斷反例是否在範圍內：

資產與接受邊界： 保護什麼，以及在哪個事件第一次被使用。
攻擊者能力： 攻擊者能控制、注入或觀察什麼。
故障規格： 目標（target）、效應（effect）、時點（timing）及每次事件預算（budget）。
可信部件： 本輪故障模型排除哪些部件，以及信任它們的依據。
環境與版本： 時鐘、reset、操作條件、設計 revision 及排除項。

接著標示證據方法：需求（requirement）、RTL 審查、模擬（simulation）、形式驗證（formal）、網表分析（netlist）、實體量測或產品測試。每種方法回答不同問題，不能互相代替。

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 與控制案例。

綜合案例：替同一顆晶片寫一份可被推翻的結論

開啟本課互動實驗

現在把後六課串起來。這顆教學晶片需要正確啟動、控制 debug、取用正確映像，並在合法環境使用 production key。審查者面前有布林矩陣、合成 campaign 與校準練習。問題是：這些教材結果能支持哪一句結論？若報告直接寫「晶片防故障攻擊已通過」，就把教學模型、未執行的工具工作與實體驗證混成了一件事。

先選一項具體 claim：在指定 target/time/effect 與事件預算內，未授權的操作不會跨越接受邊界。再把邊界寫清楚，是 debug_accept、first_fetch，還是 first key use；每一項都有自己的 oracle。來源 check_done 正確，不代表 debug 目的域已觀察；映像簽章有效，不代表 production key lifecycle 被允許。讀者應能沿 claim 找到相應條件與反例，而不是從總摘要猜作者想保護什麼。

接著為每項證據標方法。第十一、十二課提供接受政策的布林教學模型，第十三課提供合成觀察與分類，第十四課提供固定 fixture 的 campaign bookkeeping，第十五課提供合成 confusion matrix。它們可以教如何提出可驗證問題，沒有因此產生產品的 RTL simulation、formal proof、netlist analysis 或 physical measurements。下方 SVA 也仍是草案，不能把程式碼存在當成工具完成。

Claim 所需的證據	本課系列可以重算的內容	尚需的產品證據
Debug 在本次檢查被目的域觀察後才接受	第 11 課四列條件表	真實 CDC/RDC、reset 與接受 trace
Fetch/key 各依自己的交易及 lifecycle 政策	第 12 課六列矩陣	接線、獨立 oracle、映像與 key 使用證據
阻擋先於未授權 commit	第 14 課逐筆 fixture 分類	DUT/工具版本、故障刺激與重播結果
數位 effect 適用於指定實體條件	第 15 課八筆合成矩陣	可追溯量測、獨立驗證集、未知效應

先重播最可能推翻結論的那一筆

取第十四課前四筆、budget 2。try-001 在教學 edge 4 有第一個未授權 commit，之後才 alert。它足以推翻這個 fixture 所示的「每筆都及時阻擋」摘要，不能因為最終有警示而變綠。審查者應先保留第一個錯誤事件，才討論根因與修補；若先只看最後一張波形截圖，很容易把不可逆的副作用藏掉。

再看 try-004：trigger 不成立，故障未啟動。這份紀錄能證明嘗試規格中有這筆，不能證明保護擋住它。try-002 則是已故障且及時阻擋的案例；真正無故障合法接受的控制，應另讀模式中的 ctl-001，commitEdge 3、assertion PASS、cover 命中。控制與反例共同出現，才避免把「永遠不接受」誤認成完成設計。

這四筆只選到 ROM/t1、debug/t3 兩個 bins，十二格分母中另有十格未觸及。若 evidence packet 只貼「跑了四筆」，下一位工程師無法知道空格的位置。請把完整分母和逐格狀態附上，也把第十五課兩個模型外未知效應另列。未知不是通過，也不是可以從表格刪掉的零。

讓修補與原始 claim 對得上

假設審查者發現接受端只查 DUT 的 permission，reference_authorized 又直接複製同一訊號。故障若改錯 permission，DUT 與 oracle 可能一起答錯。修補需分兩層：硬體接受政策如何改變，以及 harness 的預期如何保持獨立。Oracle 本身不會阻止晶片副作用；它只讓測試有能力辨認違規。

一份完整的修補紀錄應連到反例 ID、根因、修補版本、重新執行的輸入及結果。重跑時，除了原失敗案例，也要跑合法正向控制與修補可能影響的相鄰條件。例如目的域改成等待新的 boot epoch，還需確認獨立 reset 後能重新建立合法許可。此處是驗證計畫，沒有宣稱本課已改 DUT、編譯 SVA 或取得新工具結果。

最後把未完成項留在結論旁：實體故障效果未校準、不可觀察 bins、CDC 證據缺失或 recovery 行為未驗。NIST SP 800-193 將平台韌體韌性描述為保護、偵測與安全恢復等機制，可用來提醒審查不要只看告警；它不是這份教學 campaign 的通過證書。NIST 原文。產品責任人仍需依真實證據決定剩餘風險。

綜合練習：審一份刻意不完整的 evidence packet

以下是人工設計的待審資料包，不是某產品的真實報告：「四次嘗試全部安全；try-001 已告警，try-004 無錯誤。Coverage 95%。Assertion PASS。Physical validation 待補。」附件只有一張截圖，沒有 DUT revision、工具版本、seed 或 replay command。

練習 A：逐句寫退件理由。 至少找出四項不能成立的結論，並指出每項需要什麼資料，而不只回答「證據不足」。

解答與推導： try-001 需提供第一個 commit 與 alert 的順序，現有 fixture 指出警示太晚；try-004 需有故障實際啟動證據，目前未觸發。Coverage 95% 缺分母與空 bins，既有四筆只能對應兩個 target/time bins。Assertion PASS 缺工具執行紀錄與前件發生證據，不能由截圖或未編譯草案代替。重播又缺版本、設定與輸入；實體驗證保持未完成。這些缺口各對應不同補件工作。

練習 B：寫一段範圍正確的結論。 只使用前四筆與 budget 2 的已知教學結果，保留安全、可用性、未觸發與未知狀態。

解答與推導： 可寫：「四筆合成嘗試在 budget 2 下施加四個事件，觸及兩個可觀察已啟動 bins，另十格未觸及。try-001 有未授權 commit 與遲到警示，try-002 及時阻擋，try-003 為可用性故障，try-004 未觸發。無故障控制另計；RTL/netlist/實體驗證與模型外效應尚無完成證據。」不要將這段教學結論提升為產品 release 判定。

練習 C：檢核表全勾了，能簽核嗎？ 本課互動介面的六項都打勾，畫面提醒「Checklist 欄位已齊；已列 unknowns 仍未解決，不能據此宣稱產品安全。」請說明下一位審查者仍須實際做的事。

解答與推導： 六個勾選只記錄使用者宣告的流程狀態。審查者仍須打開檔案、比對 hash 與版本、重播反例與控制、核對完整 coverage 與 unknown owner，並確認每項 claim 的證據等級。介面不會驗證檔案內容或代替產品簽核。最後分別寫出「範圍內未找到反例」「存在反例」「證據缺失」「假設無法驗證」，不要把四種狀態合成單一綠燈。

課堂推導：把結論、分母與證據逐格對起來

先備概念是「需求陳述」與「證據等級」。Claim 是在明定條件下可以被反例推翻的陳述；接受邊界是資產第一次被使用或操作 commit 的位置；trusted component 是本輪故障模型排除、仍須另有理由信任的部分。把這些詞先轉成可回答的問題：保護哪個資產？誰能做什麼故障？哪個事件算失敗？哪些部件沒有被故障測試涵蓋？

下表是填好的教學 evidence packet，以本系列結果為例。Owner 是責任角色，日期是教材案例日期，沒有指定真實人員簽核。Claim 欄寫待評估的需求，狀態欄才記錄目前能支持的結論；把需求寫進表格，不會使它自動成立。

Claim ID／接受邊界	待評估的陳述	現有證據等級	責任角色／日期	目前狀態
DBG-01／debug_accept	本次完成證據在目的域被觀察後才接受合法請求	第 11 課布林表與理想時序手算	CDC 審查者／2026-10-08	教學條件已算；產品 CDC/reset 待驗
BOOT-01／first_fetch	執行映像與當次驗證的摘要、版本、交易一致	第 12 課矩陣與 128 組枚舉	Boot 設計者／2026-10-08	教學政策已算；產品載入路徑待驗
CAM-01／commit	指定 campaign 中，阻擋先於未授權 commit	第 14 課固定 fixture	Campaign 審查者／2026-10-08	try-001 提供反例；需求未成立
PHY-01／effect mapping	數位效應能涵蓋指定實體條件	第 15 課合成矩陣與方法示範	量測負責者／2026-10-08	實體證據缺失；unknown 仍開放

從 CAM-01 開始，先沿 try-001 找出 firstBadCommitEdge = 4 與 lateAlert = true，再核對 fixture 版本與分類。這些欄位讓審查者能定位具體失敗事件。DBG-01、BOOT-01 則要提供對應的條件表及工具工作清單；PHY-01 要保留量測缺口。審查者可從任一列走到來源、重算結果與未完成工作，才算形成證據鏈。

同樣是 95%，空格可能完全不同

假設兩張不同的完整 coverage inventory，分別覆蓋 19/20 與 190/200。兩者都是 95%，卻分別有 1 格與 10 格未涵蓋；還不知道未涵蓋的格子是否恰好包括 production key、reset 或高影響故障。若不知道格子定義與風險，不能僅依較大的分母宣稱證據更強。Coverage 是清單完成度，不能直接當獨立 Bernoulli 成功率套用統計區間。

再造一個較完整的教學分母：4 target classes × 2 effects（skip、delay）× 3 time bins × 3 lifecycle 狀態，共 72 格。此分母是新增的假設 inventory，與舊十二格投影不同。原 fixture 只記 target/time；沒有替每筆提供這三個 lifecycle 的觀察，因此原來的 2/12 不能自動改寫成 2/72 的四維 coverage。

若新增兩筆明確記錄為（ROM、skip、t1、PROD）與（debug、delay、t3、PROD），並各取得有效觀察，才能在這份新 inventory 報 2/72，另 70 格未涵蓋。這兩筆是本文新造的資料條件，並非從舊 fixture 補推而來。要提升 coverage，就按空格安排實驗、記錄沒有到達目標或工具不可見的原因，再將結果填回相同版本的 inventory。

殘餘風險紀錄應讓下一步看得見

教學範例可寫：「PHY-01 尚無實體映射量測，multi-bit upset 與 power-rail coupling 未納入。目前只有課堂模型證據，產品放行狀態為未簽核。量測責任角色需提出設備、條件、獨立驗證樣本與排程；若證據仍缺失，提交產品責任人決定處理方式。」這段保留問題、責任與後續動作，沒有假裝任何人已接受風險。

真的風險接受紀錄還需產品版本、未滿足需求、影響、補救、期限、決策者與決策依據。簽名或核准是實際治理事件，應由有權責的人完成；本課只教如何準備可審查資料，不代填接受決定。資料包中的 hash 也只證明檔案身份；錯誤方法可以有正確 hash，所以內容與方法仍必須審查。

綜合計算練習： 新 72 格 inventory 已有上述兩筆有效觀察。再執行三次相同 ROM/skip/t1/PROD 的重複嘗試，都成功到達且可觀察。Attempts、有效觀察筆數與 unique covered bins 各增加多少？還有幾格未涵蓋？

完整解答： Attempts 與有效觀察各增加 3；unique covered bins 增加 0，仍為 2/72，未涵蓋仍為 70。重複案例可用來研究重現性，卻沒有增加維度覆蓋。如果一次未觸發，應扣掉有效觀察的新增數，保留 attempt 紀錄；同樣不能把它改成通過。

重算與核對

下載程式與結果 JSON 到同一資料夾，以 Python 3.8 以上執行：

python rtl-university-workbook-v1.py --output replay.json

比對 replay.json 與提供的結果檔，先核對本課的 lesson16 欄位。sourceSha256 記錄程式檔案的位元組身分，與算例正確性分開檢查；若編輯內容或把 LF 另存成 CRLF，這個值也會改變。保留原下載檔再做練習，並將學生改版另存，才能分辨方法改變與檔案改變。

下載課堂重算程式 · 查看教學 evidence packet JSON

離線互動實驗

RTL／SVA 審查方向

依 claim 組合檢查，而非共用一個通過燈號

綜合審查要同時列出 assertion、合法路徑 cover 與未完成的外部證據。以下是性質規劃表，並未產生新的工具結果：

Claim	要檢查的事件與條件	正向控制及外部證據
DBG-01	每次 `debug_accept` 都有當次、目的域應已觀察的獨立授權證據	合法啟動後能接受；另驗 CDC/RDC 與 reset 隔離
BOOT-01	`first_fetch` 的摘要、版本與交易 ID 對得上驗證；首次 key 使用另驗 slot 與生命週期	合法新映像可取指、允許的 key 可使用；另驗載入／DMA 路徑
CAM-01	整筆交易中沒有未授權 commit，不能只在 alert 同拍檢查	重播 try-001 與 ctl-001；確認 fault 實際施加與可觀察
PHY-01	SVA 只能檢查已定義的數位事件，無法產生實體 mapping 證據	需獨立量測、裝置與條件分層；unknown 保持未完成

例如 checker 在 edge 5 告警，edge 4 已輸出，單查 alert |-> !out_valid 仍可能通過。CAM-01 的需求應沿 transaction ID 檢查每次 commit 與獨立 oracle；還要定義跨 reset 的交易是否取消或保留。把各課的性質拼在一起之前，先確認它們使用相同版本、可相容的假設與各自正確的取樣域。

以下為性質草案：先定義 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？

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