簽章有效只證明某把信任金鑰簽過這些位元；它不自動證明版本可接受、量測的是即將執行的映像，或金鑰會在正確 lifecycle 釋出。
學習目標與課堂安排
完成本課後，你應能：
- 由七個授權條件推導 fetch/key 的 128 組分布。
- 依交易、摘要、版本與 key slot 定位 TOCTOU 或錯配。
- 列出版本下限更新時的斷電與恢復契約。
建議 50 分鐘的教師安排：條件定義 10 分鐘、枚舉手算 10 分鐘、錯配案例與互動 15 分鐘、斷電狀態討論 15 分鐘。時間含學生手算、互動與討論；這是教學規劃，尚未做學生課堂時間量測。
把驗證結果綁到被執行的映像
倉庫收貨時，封條、批號與箱內物必須對得上；只驗封條不能證明搬運途中沒有換箱。Secure Boot 也要把簽章者、映像摘要、硬體目標、security version、載入位置及最終取指綁在同一筆交易。類比不包含雜湊碰撞假設、DMA 競爭與微架構快取。
典型路徑是 immutable/ROM root 取得公鑰或 key identifier，驗證 manifest 與簽章，再檢查版本下限，最後鎖住相關設定並交接執行。若驗證後可寫記憶體被 DMA 改動，先前的 pass 不再代表當前 bytes。把驗證摘要與不可變 buffer/受保護載入區域關聯，並在接受端記錄 commit。OpenTitan key manager 文件將軟體 binding、版本與 sideload outputs 分成明確控制；產品仍須按實際整合判讀。Key manager。
最常漏掉的是「檢查完成」與「使用」之間的時間差：rollback counter 若只在軟體端讀一次，並發更新可能換掉版本；key release 若只看 boot_done sticky，可能沿用前一映像的授權。將 transaction ID、digest、version、lifecycle 與目的 key slot 綁定，失敗時採拒絕釋出；安全拒絕仍需避免永久不可恢復的拒絕服務。
把資產邊界定為「第一個取指」及「第一個 sideload key 使用」。First fetch 要確認簽章、版本、摘要與 transaction ID 都來自同一筆交易。Key release 還要符合 lifecycle 與目的 key slot 政策。RTL/SVA 示意不是產品 assertion，尚未接線或編譯。
尋找 TOCTOU 與 rollback
依序比較：合法新映像；簽章正確但版本低；簽署摘要為映像 A、取指卻來自映像 B；前次啟動的 boot_done sticky；debug lifecycle 下請求 production key。每種都要保留第一個違規接受邊緣及拒絕理由。
實作案例：同一個 boot_done，兩個不同資產
沿用第十一課的教學晶片，現在 ROM 要啟動映像，密碼引擎也準備使用 production key。工程師想用一個 boot_done 同時打開 CPU 取指與 sideload。先問：CPU 可以執行已簽署的除錯映像，是否表示該映像也能拿到 production key？若答案是否定的，單一 pass 就已經少了一項政策。
我們將接受端分成第一筆 instruction fetch 與第一筆 key 使用。前者保護「執行哪些位元組」，後者保護「哪個執行環境可使用哪把金鑰」。兩者共享簽章、版本與映像綁定，卻不必共享 lifecycle 許可。把兩項權限合併，會讓其中較寬的條件替另一項資產授權。
互動模型將這個問題壓成七個布林條件。令 S 為 signatureValid、V 為 versionAllowed、D 為 digestBound、L_f 為 fetchLifecycleAllowed、L_k 為 productionKeyLifecycleAllowed、T_f 為 fetchTxnBound、T_k 為 keyTxnBound。於是 fetch = S ∧ V ∧ D ∧ L_f ∧ T_f；key = S ∧ V ∧ D ∧ L_k ∧ T_k。這是授權矩陣，沒有執行密碼驗證、實際 DMA 或金鑰導出。
| 模型案例 | S | V | D | L_f | L_k | T_f | T_k | fetch | key |
|---|---|---|---|---|---|---|---|---|---|
| 目前合法映像 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| 版本過舊 | 1 | 0 | 1 | 1 | 1 | 1 | 1 | 0 | 0 |
| 驗證 A、取指 B | 1 | 1 | 0 | 1 | 1 | 1 | 1 | 0 | 0 |
| 沿用前次交易完成旗標 | 1 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 0 |
| 除錯環境請求 production key | 1 | 1 | 1 | 1 | 0 | 1 | 1 | 1 | 0 |
| 簽章無效 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 0 | 0 |
先看第五列。Fetch 的五個條件全為 1，因此允許；key 的 L_k 為 0，因此拒絕。這個結果不是矛盾，而是兩個資產有不同政策。再看第二列：簽章雖有效，版本條件為 0，兩個接受端都應拒絕。簽章回答來源與完整性問題，版本下限回答舊版本是否仍被允許；兩者不能互相代替。
逐步拆開「驗過 A，卻用到 B」
把 A 與 B 當成不同映像的符號名稱，不是實際 hash。時間 t0，ROM 驗證 A；時間 t1，控制器記下 pass；時間 t2，可寫入區域被換成 B；時間 t3，CPU 從該區域取第一條指令。即使 pass 仍為 1，t3 使用的位元組也沒有被那次驗證涵蓋。這是 TOCTOU 的教學反例，不是本課已在 RTL 或晶片上重現的攻擊。
修正時要先選擇能維持的契約。若驗證後的載入區域禁止修改，就需列出 CPU、DMA、debug 與其他 bus master 是否都受同一保護，以及鎖定發生在何時。若採重新驗證，則要說明驗證與使用之間如何保持一致；單純在另一個較早時刻再算一次 digest，仍可能留下新的時間窗。修補不是增加一個 pass bit，而是讓證據對應到接受時實際使用的物件。
同樣地，transaction ID 用來分辨「這一次」與「上一次」。假設前次啟動 A 已經成功，當次 boot_done 保持為 1；新一輪 B 啟動時若沒有撤銷舊授權，B 就可能借用 A 的完成狀態。模型第四列讓 T_f、T_k 同時為 0，以便讀者看到兩個接受端都該拒絕。真實 ID 的寬度、回繞、reset 行為與跨域傳送仍須另外設計；模型並未證明這些細節。
金鑰端還要記錄目的 key slot 與首次使用，而不只記錄「釋出命令已送出」。Sideload 路徑可避免金鑰透過一般軟體介面讀出，但沒有因此消除授權問題。若接收引擎可保存先前的有效旗標，新的映像仍可能在錯誤的交易世代使用舊授權。審查時應沿著命令、接收確認與實際使用追蹤，找出真正不可逆的資產邊界。
延伸練習：為每個拒絕寫出原因
練習 A：最小條件變更。 從第一列開始，每次只讓 V、D、T_f 或 T_k 其中一項變成 0。先手算 fetch 與 key；V、D 對照上表，T_f、T_k 則依公式推導。哪一項只應影響其中一個接受端？
解答與推導： V 或 D 為 0 時兩者都拒絕；T_f 為 0 時 fetch 拒絕而 key 可維持允許；T_k 為 0 時 key 拒絕而 fetch 可維持允許。後兩種是依公式推導的新增練習，既有六個預設案例沒有逐一提供這兩列。回答時應指出它們是矩陣推論，避免說成模型新增了按鈕。
練習 B：修補 sticky flag。 有人提議在新 boot 開始時清除 boot_done。這是否已足以處理 producer 重啟而 key consumer 未重啟的情況？
解答與推導： 還需要檢查 consumer 是否保存舊許可、在途訊息是否重新送達，以及 ID/epoch 是否一致。來源清零只改變來源狀態，不能保證目的端撤銷。合法新啟動也必須能重新建立授權，否則修補可能造成永久拒絕服務。
練習 C：找出自我證明。 Testbench 直接把 DUT 的 signature_ok 接成 reference_signature_valid，故障又可能翻動 signature_ok。Assertion 沒報錯，能否說明簽章政策安全？
解答與推導： 不能。受故障影響的訊號同時控制接受與預期結果，可能一起被改錯。獨立 oracle 應依可信輸入與政策產生預期，並放在指定故障影響錐外；還要用簽章無效的負向案例與目前合法映像的正向控制檢查它。這些是 harness 的設計要求，本課沒有執行真實簽章演算法或 formal proof。
課堂推導：六個預設案例之外的 128 組條件
先備知識是布林 AND、集合交集，以及持久版本下限。上方七個條件若各自取 0 或 1，共有 2⁷ = 128 組；這是布林輸入空間的枚舉，並非宣稱所有組合都能在某產品到達。Fetch 要求五個條件皆為 1，留下 L_k、T_k 兩個自由變數，因此共有 2² = 4 組允許 fetch。Key 同理也有 4 組。
兩個接受端都允許時，七個條件全為 1，只有一組。因此只允許 fetch 是 4 − 1 = 3 組，只允許 key 也是 3 組；皆拒絕為 128 − (1 + 3 + 3) = 121 組。先用交集移除重複，才計算剩餘集合；不能把兩個 4 相加後，誤認為有八組至少一端允許。
| fetch | key | 組合數 | 推導 |
|---|---|---|---|
| 1 | 1 | 1 | 七條件全為 1 |
| 1 | 0 | 3 | 四組 fetch 減共同一組 |
| 0 | 1 | 3 | 四組 key 減共同一組 |
| 0 | 0 | 121 | 128 減至少一端允許的七組 |
只允許 fetch 的三組，其 L_k/T_k 分別為 0/0、0/1、1/0，其餘五條件皆為 1。前兩組缺金鑰 lifecycle 許可，最後一組缺金鑰交易綁定。這比只讀 debug 預設列更能說明「CPU 能執行」與「密碼引擎能用 key」的差別。反過來，只允許 key 的列只是獨立布林模型中的組合；真實開機協定若禁止該狀態，需將不可達假設寫進驗證。
Rollback 下限與斷電，是另一張狀態表
設持久 security version floor = 5。版本 4 即使簽章有效仍被拒絕；版本 6 可通過版本條件。現在還要決定何時把 floor 提升到 6。若在新映像尚未具備可用恢復路徑前先提高下限，斷電或映像失敗可能讓唯一能啟動的版本 5 也被拒絕。若太晚提高，則可能在那個時間窗仍允許回到 5。安全與恢復須一起設計，這裡沒有替產品指定唯一正確的更新順序。
一份更新契約至少需定義：新映像的完整性與授權；待啟動、成功確認與失敗恢復狀態；counter 寫入的原子性與持久性；每個可斷電點重新上電後選哪個映像。Recovery 映像也有自己的授權與版本政策。學生應把每個斷電點列成輸入條件，檢查是否出現未授權執行或無法恢復的合法服務，而不是只問「先寫 counter 還是後寫」。
TOCTOU 可再比較兩種載入路徑：驗證 SRAM 中的副本並由同一份副本執行，前提是從驗證到使用期間所有 writer 都受保護；直接從 flash 執行的 XIP 路徑，驗證讀取與 CPU 取指分屬不同存取，需另保持內容與映射一致。SRAM 或 XIP 的名稱都不會自動滿足這些條件。多階段 boot 也要為每個交接建立映像、交易、版本與 key 目的的綁定，不能把單一映像矩陣套到所有階段。
計算與設計練習： 把 key slot 綁定 K_s 加成第八個布林條件，但它只限制 key。現在兩端皆允許、只 fetch、只 key、兩端皆拒絕各有幾組？如果 K_s 為 0，原本都允許的七條件還能得到 key 嗎？
完整解答： 八個輸入有 256 組。Fetch 仍固定五條件，另外三條件自由，允許八組；key 固定原五條件再加 K_s，另外兩條件自由，允許四組。交集為所有八條件皆為 1 的一組；所以四個數量是 1、7、3、245。K_s = 0 時，fetch 可以允許，但 key 必須拒絕。這是本文新增的推導模型，既有七條件 HTML 沒有實作第八個輸入。
一份明定契約的斷電狀態表
以下另造雙槽更新例子：A 為已驗證版本 5；B 將更新為版本 6；版本下限 F 起始為 5。假設映像及選槽中繼資料可驗證，confirmed 紀錄與 F 寫入各有原子性／持久性，且獨立恢復映像 R 的版本為 6、可用且另經授權。這些是假設條件，現有互動模型沒有實作儲存或斷電。
契約是：B 完整寫入並驗證後才標為 pending；試開成功且 confirmed 紀錄已持久化後才提升 F。每次重啟仍驗映像及版本；不靠前次 pass。依下表決定選槽：
| 斷電點 | 持久狀態／F | 重啟選擇與拒絕 | 未授權執行／恢復性 |
|---|---|---|---|
| 寫 B 前 | A confirmed；F=5 | 驗證後選 A5 | 沒有未授權執行；A 可服務 |
| B 未寫完 | B 不完整；F=5 | 拒絕 B，驗證後選 A5 | 沒有未授權執行；A 可服務 |
| B 驗證且 pending 已持久化 | A5/B6；F=5 | 試 B6；失敗可依此契約回 A5 | A5 在此 F 下仍被允許；至少有合法恢復路徑 |
| B confirmed 後、提升 F 前 | B confirmed；F=5 | 驗證後選 B6；必要時選 R6 | 未授權路徑仍拒絕；B 或 R 可恢復 |
| 原子 F 寫入途中 | B confirmed；F 只能為 5 或 6 | 驗證後選 B6；必要時選 R6 | 兩個可能的 F 都允許版本 6 |
| F=6 已持久化 | B confirmed；F=6 | 驗證後選 B6 或 R6；拒絕 A5 | 不退回版本 5；B/R 可恢復 |
「可恢復」仰賴假設中的映像可用及驗證成功；若 B 與 R 都失效，就要拒絕執行並記錄服務損失。如果 F 寫入可能落到第三種不合法值，原子性假設便不成立，必須另外定義檢出及恢復。表中 F=5 的中途狀態沒有宣稱版本 6 一旦試開就立刻禁止 5；政策何時承諾新的版本下限要寫清楚。
斷電練習： 若把「提升 F」移到 B 完整寫入前，F 已為 6，但 B 不完整、A 仍為 5，且沒有 R6，哪項需求失敗？
解答： B 驗證失敗；A 因版本低於 F 被拒。安全拒絕可以維持，合法服務卻沒有恢復路徑。應先建立可驗證的新版與恢復條件，再按明定契約完成不可逆更新；不能為了救可用性而偷偷繞過版本下限。
重算與核對
下載程式與結果 JSON 到同一資料夾，以 Python 3.8 以上執行：
python rtl-university-workbook-v1.py --output replay.json比對 replay.json 與提供的結果檔，先核對本課的 lesson12 欄位。sourceSha256 記錄程式檔案的位元組身分，與算例正確性分開檢查；若編輯內容或把 LF 另存成 CRLF，這個值也會改變。保留原下載檔再做練習，並將學生改版另存，才能分辨方法改變與檔案改變。
離線互動實驗
RTL／SVA 審查方向
以下為性質草案：先定義 harness 的 transaction、reset 與 oracle，並確認取樣邊界，再接入設計；尚未編譯或證明。
assert property (@(posedge clk) disable iff (!rst_n)
key_release |-> signature_ok && reference_signature_valid && active_txn_id == reference_txn_id &&
active_digest == reference_digest && active_version >= security_version_floor &&
reference_key_release_allowed && key_slot == reference_key_slot);
assert property (@(posedge clk) disable iff (!rst_n)
first_fetch |-> fetch_digest == reference_digest && fetch_txn_id == reference_txn_id &&
signature_ok && reference_signature_valid &&
fetch_version >= security_version_floor && reference_fetch_policy_ok);
cover property (@(posedge clk) disable iff (!rst_n)
key_release && signature_ok && reference_signature_valid && reference_key_release_allowed);
cover property (@(posedge clk) disable iff (!rst_n)
first_fetch && signature_ok && reference_signature_valid && reference_fetch_policy_ok);reference_*、reference_signature_valid 與 security_version_floor 必須來自獨立 harness oracle，不可直接複製 DUT 的 sticky/pass 訊號。first_fetch 與 key_release 若位於不同時鐘域，須各自在事件所在時域檢查；本草案未證明 CDC。
此片段不證明 CDC、timing、side-channel 或實體注入；需由各自工具與測量提供證據。
檢核問題
- 辨認：有效簽章證明了什麼，還有哪些決策未完成？ 推理： 它在指定金鑰下驗證一串已簽署位元。版本政策、目標綁定、最後 fetch 的位元組，以及金鑰釋出政策仍要分開檢查。
- 比較：security version floor 與簽章驗證有何不同？ 推理： 舊映像也可能有有效簽章。Version floor 依政策拒絕 rollback；它本身不驗證映像內容。
- 情境：DMA 能在第一筆 instruction fetch 前修改已驗證 buffer。設計要綁定或保護什麼？ 推理： Digest 必須對應 CPU 最後 fetch 的相同位元組。可鎖定載入區域，或在實際使用邊界重新驗證。
- 故障診斷：sticky boot_done 來自上一筆 boot transaction。為什麼它不足以授權 key release？ 推理： 這個 bit 沒有指出目前映像或 transaction。釋出時要綁定 transaction ID、digest、lifecycle、version 與目的 key slot。
- 設計風險／轉移：debug lifecycle 可 fetch 已簽署映像，但不可使用 production sideload key。應分別記錄哪些結果？ 推理： 第一筆 fetch 與第一筆 key release 要分開記錄。Fetch 可以允許，production key release 同時維持拒絕。
延伸閱讀
OpenTitan Key Manager · NIST SP 800-193
MY ACADEMY · LESSON FILM
教學影片
影片依序說明本課的資料路徑。看完一段，可以回到下面的互動練習，改變輸入或故障條件。動畫呈現教學模型；它沒有替代 RTL 模擬。
左右滑動影片，或用方向鍵查看圖卡。
圖卡的範圍說明
教學模型 · 非 RTL 模擬或晶片實測
性質草案未編譯／證明；不替代 CDC、side-channel 或實體注入證據
旁白使用合成聲音。互動教學與動畫均有模型邊界；請以本課的來源與驗證範圍解讀結果。
Wrap-up｜把這一課帶回設計審查
- 威脅模型與成立條件
單筆啟動交易含映像摘要、簽章結果、版本下限、lifecycle 與 key slot；最終取指/釋出是資產邊界。
- 失效原因
驗證結果和後續使用對象脫鉤，或 rollback / 前次 sticky 讓過期授權沿用。
- 防護方法
以不可變 transaction context 綁定 bytes、version、lifecycle、key slot，失敗預設拒絕，並保護接受端。
- 驗證方式與待做檢查
對合法、過期、篡改、映像替換及 lifecycle 不符逐案檢查；RTL/簽章與記憶體整合尚未實測。
- 防護界線與未驗證項目
未分析金鑰管理政策、供應鏈根信任、side-channel、實體 key vault 與 recovery image 的產品細節。
換個情境再想一次
加入 rollback counter 更新與並發 DMA；說明何處必須鎖定內容，以及何時才可釋出 sideload key。
以上整理對照本課的教學案例、參考資料與實驗範圍；未列為已完成的驗證，都是後續工作。