開機電路剛完成簽章驗證。映像不合格,結果暫存器保存了 0。CPU 隨後提出取指請求,但在這之前,故障已把保存值改成 1。驗證器算對了,放行電路卻讀到另一個答案。
要保護這個結果,不能只問「暫存器還讀得出值嗎」。完整性保護要能辨認指定範圍內的改動,並在錯誤值被使用前阻擋。 多存幾個檢查位元,是一種做法;但多存並不代表所有故障都能被看見。
本課用同一個放行問題,比較 parity、互補編碼與錯誤修正碼。每看一種方式,都先確認它會拒絕哪些改動,再試著把「失敗」改成仍然合法的「通過」。最後用小實驗重現這些反例。
先備知識是暫存器、基本邏輯與時脈取樣。第二課說明故障模型,可先閱讀或隨時回查。本課的電路是教學設計;已執行 Python 練習,尚未完成 RTL 模擬、綜合、形式證明或矽上驗證。
1. 多存幾個位元,有什麼用途?
想像學校的領餐券有資料格與檢查格。資料格記這次能否領餐,檢查格用來辨認券上指定的改動。只有 0、1 一格時,改完仍是一個合法值;加入檢查格,某些組合才成為非法券。它們對應資料位元與檢查位元組成的碼字。券印得合規,仍可能印了錯的資格;本課不把碼字合法當成真正有權領餐。
只用一個 bit 表示授權,0 與 1 都是合法值。它被翻轉後,讀取端沒有第三種值可以拿來辨認錯誤。完整性編碼加入檢查位元,把資料與檢查值一起保存;這整組值稱為「碼字」。圖中的 DFF 是保存位元的電路。
設計者先定義合法碼字。其他組合留作非法值,讓檢查電路辨認。指定的故障若把保存值改成非法碼字,電路就能報錯;若改成另一個合法碼字,單靠格式檢查便看不出來。
這正是本課要逐一找的反例:原本合法的失敗值,能否變成合法的通過值?碼字合法,並不代表授權正確。 授權還取決於這次映像是否通過政策,以及結果如何產生與傳到下游。
CPU 讀取程式指令,稱為「取指」。本課追蹤一個簡化的取指介面。accepted_commit 表示下游已接受取指。它不是完整 CPU 的指令退休事件。
2. 先說清楚,這次故障打在哪裡
這次先限定只改已經保存的券,第 3 拍改,第 4、6 拍各領一次;原始資格簿、檢查員與窗口先可信。一個mask圈出同一事件動到的格子,主表會分別統計翻一格、兩格等預算。兩次領餐不是兩次改券。若改發券前的資格或最後交餐許可,那是另外的target;紙券也不表示真實晶片位元彼此距離多遠。
故障注入是故意擾動電路的測試方法。故障模型則規定擾動的範圍。本課先只改保存碼字的暫存器。每次實驗只發生一次注入事件。
一次事件可以翻轉多個位元。實驗會分開測試各種位元數。這些是我們選定的模型條件。它們不是實體攻擊能力的量測結果。
本課用 edge 標示時脈取樣的時刻。Clock/reset 指時脈與重置。
| 模型欄位 | 本課的設定 |
|---|---|
| 保護目標 | 未授權映像不得取得 accepted_commit |
| 正常排程 | edge 0 重置;edge 2 保存驗證結果 |
| 故障時機 | edge 3 正常更新後,翻轉保存的位元 |
| 故障期間 | 改過的值保留;後面不覆寫、不自動修復 |
| 故障預算 | 一次事件、一個碼字暫存器;各組分別改 1~4 bits |
| 接受時機 | edge 4、6 有請求;請求有效且下游可接收 |
| 觀察期限 | edge 0~7;兩次請求共用一次嘗試 |
| 可信範圍 | 編碼、檢查、阻擋、錯誤歷史及完成旗標不受擾 |
| 其他可信範圍 | 映像、政策、獨立 reference、clock/reset、握手及接受端不受擾 |
每個 edge 先判斷是否接受取指。暫存器再更新狀態。注入器最後改寫新狀態。故障因此能留到下一次請求。
獨立 reference 記錄原本應有的授權。reference 不讀受擾的碼字。實驗用它判斷是否越權。這次映像固定且未授權。
本課假設,故障只影響目標暫存器。 檢查與控制電路都保持正常。實體擾動可能同時影響多處。產品團隊必須另行驗證這個邊界。
先固定邊界,才能比較三種編碼本身的差異。第 8 節會另外把來源與最終 grant 列為目標,看先前的結論如何改變。那些是分開的實驗,不會和本節的儲存故障同時注入。
3. Parity:用一個位元檢查奇偶
領餐券若規定整張券的 1 必須為偶數,00000 合規卻表示不能領餐。只改資料格成 00001,會有奇數個 1,檢查格與資料不合;若資料格與保存的檢查格一起改成 10001,又有偶數個 1,卻表示可領餐。這正是 parity 的 0x11 反例。檢查員若看著改過的資料重新補章,相符就失去原保存值的證據;故事也沒有讓 parity 辨認所有雙格改動。
Parity 用一個檢查位元記錄資料的奇偶性。本課採偶同位元檢查:整個碼字中,1 的數量必須為偶數。先留意它檢查的是奇偶,不是每個 bit 原本的值。
本課保存四個資料位元。電路另外保存一個 parity 位元。資料 0000 表示失敗。資料 0001 表示通過。其他資料值都不得放行。
失敗碼字是 00000。翻轉一個 bit,1 的數量變成奇數,檢查便會報錯。這讓一個新增的檢查位元,能涵蓋任何單一儲存位元的翻轉;但它不會告訴你哪一位錯了。
翻轉兩個 bit,奇偶性可能仍然符合。把資料最低位與 parity 位一起翻轉,00000 就變成 10001。這是合法的通過碼字,parity 不會報錯。少量冗餘能抓到單 bit,並不代表它能守住這個兩 bit 反例。
XOR 是互斥或運算。它可用來計算 1 的奇偶數量。Verilog 的 ^data_q 會縮減整組位元。下面的檢查不會改寫保存值。
AND 要求所有條件同時成立。NOT 則把 0 與 1 互換。圖中的邏輯區塊用這些名稱標示。
// Store the check bit when the trusted result is written.
if (write_en) begin
data_q <= data_i;
parity_q <= ^data_i;
end
assign local_bad = (^data_q) ^ parity_q;
assign decoded_pass = (data_q == 4'b0001);
電路必須一起保存資料與檢查值。如果電路從受擾資料重新產生 parity,兩者會再次相符。這種接法無法檢查先前保存值的改動。
接著看互補編碼,問題仍相同:哪種翻轉會落到非法值?哪種會直接變成合法通過?換一種儲存方式,不會改變這兩個判斷問題。
4. 互補編碼:保存兩個相反的值
換成兩格領餐券,01 表示拒絕、10 表示准許。規則要求兩格相反;改一格得到 00 或 11,可以拒絕,兩格一起改卻得到另一張合規券。這對應保存互補位元。若窗口只把同一格影印後反色,原格改了,影印也跟著改,沒有第二份保存證據;有兩格不代表有兩次獨立資格審核。
互補編碼把一個判斷存成兩個相反的位元。本課用 01 表示失敗,10 表示通過;00 與 11 都非法。讀取端可以檢查兩者是否仍互補,再完整比對通過碼字。
從 01 翻轉一個 bit,只能得到 00 或 11,因此能被拒絕。兩個 bit 一起翻轉,則直接得到 10。兩份保存值仍然互補,授權卻已變錯。檢查互補關係與檢查授權來源,是不同工作。
讀取端若只把同一個 Q 反相,便沒有第二份保存值。Q 是暫存器的輸出。故障若改了 Q,反相線也會跟著改。這兩條線不能提供同樣的保存檢查。
兩份暫存器也可能共用同一個來源。如果來源先變錯,編碼器會保存合法的錯誤碼字。因此,互補關係不能證明來源授權正確。
這種編碼增加的,是對指定儲存改動的辨認能力。它沒有提供兩次獨立的簽章驗證。若產品宣稱有兩條獨立保護路徑,還要查它們的來源、時脈、reset 與綜合後結構。
5. SECDED:能修正,為什麼還會放錯?
再換成八格券,檢查員依固定規則修補『看起來像一格印錯』的券。00000000 被改三格成 00000111,規則卻把它歸類成可修正,補上第八位置後成 10000111,也就是可領餐的 0x87。這對應本課 SECDED 誤修正。CE 表示檢查員的分類,沒有目擊實際改了幾格;能修一格的規則,不能延伸成任何券都會修回原資格。
前兩種方式發現錯誤後,只能拒絕使用。錯誤修正碼加入更多檢查位元,讓解碼器在指定錯誤範圍內找回原值。英文縮寫也是 ECC;本課指 Error-correcting Code,不是橢圓曲線密碼。
SECDED 表示單 bit 修正、雙 bit 偵測。這個能力有範圍:不能把「能修正一位」延伸成「任何故障都會被正確修復」。如果實際故障超出範圍,解碼器可能把它歸到錯誤的類別。
本課使用自訂的 extended Hamming (8,4)。它用八個位元保存四個資料位元。讀者先記住兩個值:失敗是 0x00;通過是 0x87。0x 表示十六進位數。
解碼器依 syndrome 與整體 parity 產生 CE、UE。CE 是「解碼器判定可修正」,UE 是「判定不可修正」。它看見的是現在的碼字,不是攻擊發生的過程。因此,CE 不證明實際只翻轉了一個位元。
三個位元把 0x00 改成 0x07 時,檢查結果與某種單 bit 錯誤相符。解碼器於是報 CE,再翻轉位置 8,得到通過碼字 0x87。這是一個指定 pattern 的誤修正反例,不是說所有三 bit 翻轉都得到相同結果。詳細配置放在下方展開區。
現在比較兩種使用政策。「修正後繼續」會使用修正值。它只在 UE 時拒絕取指。上述 CE 反例因此會越權。
「遇錯即拒絕」會拒絕 CE 與 UE。放行判斷也不使用修正值。它能擋住上述三位元反例。不過,四個指定位置一起翻轉,仍可能形成合法通過碼字。
兩種政策的差別,是是否信任錯誤後的修正值。對授權資料,修正後繼續可能改善可用性,卻需要證明錯誤模型適用。遇錯即拒絕較保守,也可能阻擋原本合法的工作。第 7 節會分別列出越權與合法映像受阻的結果。
想知道 0x07 為何得到 CE?展開位元配置。
八個位置由 1 數到 8。它們對應儲存位元 0~7。資料放在位置 3、5、6、7。檢查位放在位置 1、2、4、8。
| 位置 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 |
|---|---|---|---|---|---|---|---|---|
| 用途 | p1 | p2 | d0 | p4 | d1 | d2 | d3 | p8 |
S 稱為 syndrome,即檢查結果的索引。S 由三個檢查結果組成。P 是八個位元的整體 parity。完整計算式可查看下載的程式。
| S | P | 解碼器的動作 |
|---|---|---|
| 0 | 0 | 不報 CE 或 UE |
| 0 | 1 | 報 CE;翻轉位置 8 |
| 非 0 | 1 | 報 CE;翻轉位置 S |
| 非 0 | 0 | 報 UE;不做單位元修正 |
0x07 翻轉位置 1、2、3。三個位置的檢查索引互相抵消。所以 S 是 0,P 是 1。解碼器便翻轉位置 8。0x87 的二進位顯示是 10000111。這裡由 bit 7 排到 bit 0。
兩個不同合法碼字至少相差四個位元。這稱為最小碼距 4。碼距可描述原始碼字的分離程度。修正後的放行行為仍須另行分析。
OpenTitan 的 OTBN 採用另一種碼。它使用 (39,32) Hsiao 碼做完整性檢查。OTBN 不會自動修正這些錯誤。作者的討論也指出多位元誤修正風險。本課借它說明政策選擇,未複製 OTBN 碼字。OTBN 設計說明、OpenTitan 原始設計討論
不依賴圖,算一次 SECDED 誤修正
給檢查員一張只含現在八格的券,他算出 S=0、P=1,便依表翻第 8 位置。他不知道這張券從原本 0x00 被改了第 1、2、3 位置。這讓『修正後繼續領』與『報 CE 也先拒絕』有不同結果。計算syndrome對應檢查分組,不是老師猜出攻擊歷史;直接拿合法0x87來,兩種格式檢查都可能無異常。
把 syndrome 的三個檢查位寫成 s1、s2、s4。s1 檢查位置 1、3、5、7;s2 檢查 2、3、6、7;s4 檢查 4、5、6、7。每組做 XOR,S=s1+2×s2+4×s4。P 對全部八位做 XOR。這裡的加法是在組合檢查索引,不是再次計算 parity。
對 0x07,只有位置 1、2、3 是 1。因此 s1=1 XOR 1=0,s2=1 XOR 1=0,s4=0;S=0。三個 1 讓 P=1。解碼器只能看見 (S,P)=(0,1),便依表翻轉位置 8,得到 00000111 XOR 10000000 = 10000111,也就是 0x87。位置 3 的 d0=1,其他資料位=0,解碼資料為 0001(通過)。
現在比較使用政策。「修正後繼續」看到 CE=1、UE=0,仍使用 0001;「遇錯即拒絕」把 CE 也接到阻擋,拒絕這次接受。不過直接翻四位得到 0x87 時,S=P=0,兩者都看不到格式錯誤。這串計算把碼距、解碼器判定與放行政策分開;實驗只涉及指定保存位元,不能據此推論來源或最後 grant 已受保護。
6. 發現錯誤後,要在什麼時候阻擋?
第 4 拍窗口已看出領餐券不合規,值班簿卻要等這次鐘響後才記下『曾出錯』。只看舊值班簿,第一份餐仍可能先交出去。當下的拒絕對應 local_bad,之後留下的紀錄對應 sticky。兩者同時參與放行,才守住本課指定時序;故事假設檢查結果在交餐前已到,不能替真實傳播延遲或拍內glitch作保。
看出錯誤之後,還要決定何時阻擋。local_bad 是當下的檢查結果;err_sticky_q 則保存曾經報錯的歷史。兩者時間不同,不能只用「已有錯誤處理」一語帶過。
故障在 edge 3 更新後產生,下一次請求在 edge 4 到達。檢查電路已看到錯誤,sticky 的舊值卻仍是 0。它要等 edge 4 更新後才記住異常。若接受端只看舊 sticky,而且受擾資料解成 PASS,第一個請求仍可能通過;事後記錄不能撤回這次接受。例如 parity 的失敗碼字 00000 被 mask=00001 改成資料 0001、parity 0:decoded_pass=1、local_bad=1,edge 4 前 sticky=0,valid=ready=1。只靠舊 sticky 便會接受。
電路應讓 local_bad 直接參與放行。Sticky 則持續記住錯誤。下面兩種 ECC 政策共用這個阻擋位置。
本課主表的儲存錯誤會持續存在,所以被偵測後,local_bad 也持續成立;表內並未另外證明 sticky 增加了攔阻案例。Sticky 的一般用途,是在異常消失或狀態被改寫後仍保留紀錄。那種情境需要另設測試,不能冒充本次已有的結果。
checked_q 記錄驗證是否完成。local_bad 是當下的錯誤檢查結果。fetch_valid 表示請求有效。fetch_ready 表示下游可接受請求。
raw_data 是讀出的未修正資料。corrected_data 是修正後的資料。政策決定 selected_data 要使用哪一份。
assign local_bad = ue | (ECC_REJECT_CE && ce);
assign selected_data = ECC_REJECT_CE ? raw_data : corrected_data;
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) err_sticky_q <= 1'b0;
else err_sticky_q <= err_sticky_q | local_bad;
assign grant = checked_q && (selected_data == 4'b0001)
&& !local_bad && !err_sticky_q;
assign accepted_commit = fetch_valid && fetch_ready && grant;
這段電路在理想取樣模型中會及時阻擋。產品仍需檢查傳播延遲。檢查結果必須在接受取樣前穩定。拍內短暫脈衝也需要另外驗證。
SVA 是描述時序條件的驗證語言。下面的 assert 要求每次接受都有授權。Cover 則確認正常授權仍可取指。兩者都需要完整測試環境。
assert property (@(posedge clk) disable iff (!rst_n)
accepted_commit |-> (reference_complete && reference_pass));
cover property (@(posedge clk) disable iff (!rst_n)
reference_complete && reference_pass && accepted_commit);
7. 先重跑三個反例,再看完整結果
把同一張不準領餐的券各重新印一次,分別改 parity 的 0x11、互補券的 0x03 和八格券的 0x07。先預測窗口會看到什么,再比較原值、修正值和交餐紀錄。342 條軌跡是指定券與mask的枚舉,不是342次真人闖關;合法券受阻也要另記,才看得出保守拒絕政策的服務代價。
下載 Python 練習與 RTL 範例。Python 只使用標準函式庫。以下指令會產生結果檔。
python lesson03_register_integrity.py --output-dir lesson03-results
先預測三個結果。Parity 使用 mask 0x11。互補編碼使用 mask 0x03。Hamming 使用 mask 0x07。Mask 指定哪些位元要翻轉。
前兩個案例會變成合法通過碼字。第三個案例會觸發 CE。修正後繼續的版本仍會越權。遇錯即拒絕的版本則會阻擋。
先看一條 trace 的順序,再看總表。Edge 3 之後碼字怎麼變?Edge 4 前檢查器報什麼?最後 grant 使用的是原值還是修正值?這三步能解釋同一個 fault 為何在兩種政策下得到不同結果。
我們已執行 Python 實驗。342 條儲存故障軌跡中,8 條出現越權。這些數字只是本課模型的枚舉結果。它們不是矽上攻擊成功率。
展開完整枚舉表與驗證範圍。
每列各自固定翻轉位元數。每條軌跡只用一個 mask。兩次接受不會另算成兩條軌跡。
| 版本 | 翻轉 bits | 軌跡數 | 越權軌跡數 |
|---|---|---|---|
| Parity | 1 | 5 | 0 |
| Parity | 2 | 10 | 1 |
| 互補編碼 | 1 | 2 | 0 |
| 互補編碼 | 2 | 1 | 1 |
| 修正後繼續 | 1 | 8 | 0 |
| 修正後繼續 | 2 | 28 | 0 |
| 修正後繼續 | 3 | 56 | 4 |
| 修正後繼續 | 4 | 70 | 1 |
| 遇錯即拒絕 | 1 | 8 | 0 |
| 遇錯即拒絕 | 2 | 28 | 0 |
| 遇錯即拒絕 | 3 | 56 | 0 |
| 遇錯即拒絕 | 4 | 70 | 1 |
程式另做了 3,112 個碼字檢查。它遍歷所有資料值與指定翻轉數。獨立碼字表用來檢查修正結果。這部分不同於 342 條取指軌跡。
程式也跑了 8 條無故障控制。未授權控制都沒有取指。授權控制都接受 edge 4、6。
另外 23 條實驗使用授權映像。它們各翻轉一個儲存位元。其中 8 條修正後繼續仍能取指。其他 15 條被阻擋。這提醒我們也要評估可用性。
上游故障與最終 grant 故障各跑 4 條。它們是分開的擴大範圍實驗。Sticky 延遲反例也另外計數。這些案例沒有混入 342 條主表。
RTL 範例含測試用的注入入口。正式電路必須移除這些入口。測試環境須限制 mask 的寬度與數量。Parity 只允許最低五位。互補編碼只允許最低兩位。
本課已跑 Python,尚未跑 RTL 模擬。綜合、形式證明與矽上測試也未執行。SVA 範例不構成已完成的證明。
8. 暫存器之外,還有哪些缺口?
如果發券前的資格輸入被換成可領餐,列印機能印出完全合規的錯券。若券仍正確,交餐許可卻被改成真,也會交錯餐。這分別對應source與grant的擴大實驗,不能加入保存券主表仍說只改儲存。窗口與reference仍可信;也沒有把放三張券在桌上當成晶片實物獨立性的證據。
儲存檢查只能處理指定的儲存問題。它不能自行補上所有授權缺口。我們再看兩個不同的故障位置。
第一個位置是上游 auth_ok_i。故障在 edge 2 保存結果前,把它改成 1。編碼器便產生合法的通過碼字。四種版本都會越權。
第二個位置是最終 grant。故障在 edge 4 把阻擋值改成放行值。下游便接受第一次取指。上游碼字仍然正確。四種版本都擋不住這個額外目標。
這裡仍假設下游握手與接受機制可信。實驗改的是接受之前的 grant,不是下游內部 buffer 或 fetch_ready。不能據此宣稱 consumer 內所有位置都已測過。
多存幾個位元,也不保證實體獨立。暫存器可能靠得很近。它們也可能共用時脈、重置或來源。綜合工具還可能合併重複邏輯。
OpenTitan 的實作指南討論了這些問題。它建議局部反應配合告警。它也提醒冗餘邏輯可能被綜合合併。設計團隊應檢查綜合後的實際結構。OpenTitan 硬體實作指南
9. 帶著一個問題讀論文
看另一套領餐券研究,先問它准許改幾格,查的是發券、保存還是交餐,修補後是否仍准許領餐。這些問題對應位元預算、資料路徑與ECC使用政策。論文中的實物實驗若發現更多格受影響,會改變模型前提;它沒有直接證明本課某個mask在任何晶片都能做到。
先讀模型,再讀防護結果。讀者可用下面四個問題做筆記。每個問題都對應本課的一個邊界。
- 儲存保護有沒有涵蓋整條資料路徑? Tollec 等人的研究分析安全 CPU 的故障保護邊界。作者也修正了 OpenTitan 的相關問題。讀者可追查暫存器檔案的保護位置。Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults
- 實體故障會超出位元預算嗎? Bartkewitz 等人以雷射測試碼字防護。研究對象是 40 nm ASIC 的 SKINNY 實作。結果提醒讀者核對實體故障與模型假設。本課沒有重現其實驗。Beware of Insufficient Redundancy
- 工具結果涵蓋哪些位置? HOST 2020 的 VerFI 用於分析故障行為。讀者應先記下故障模型與測試條件。工具的有限結果不能直接變成實體保證。Cryptographic Fault Diagnosis using VerFI
- 增加一個目標後,結果如何改變? SYNFI 的 OpenTitan 案例分開分析輸出與上游控制。讀者可對照本課的來源故障。SYNFI 作者版,第 4.1.2 節
Grok 提供獨立的文獻研究。Claude 檢查反例,並審查完成的教材。Codex 查證原始來源並製作教材。外部意見提供檢查線索。上表數字則來自本課實際執行的 Python。
10. 換一個假設,再選保護方式
先只准改一格,再準同一事件改三格,最後把發券來源也列進目標;同一窗口規則會面對不同問題。只准一格時可修回原資格,三格0x07可能誤修,來源錯了卻能印合法券。選保護方式要跟著這三張模型卡走;沒有把『加了ECC』當成校規已經完成,也要記合法學生可能領不到餐的代價。
先假設故障只能翻轉一個儲存位元。Parity 與互補編碼都能看出異常。Hamming 也能把資料修回原值。設計者仍要決定,錯誤後能否繼續操作。
再允許同一事件翻轉三個位元。修正後繼續便出現新的越權反例。如果授權結果採用遇錯即拒絕,本課模型就能擋住它。這項結果仍依賴可信的檢查與阻擋電路。
最後,把來源也列為故障目標。合法碼字就可能從錯誤來源產生。設計者此時需要新的授權綁定。下一課會用多位元控制訊號繼續分析。
回到開場,加入檢查位元後,判斷是否放行仍要看 fault 的位置、位元數與政策。先選模型,再選編碼,最後追到接受點;不能只在規格上寫「有 ECC」。下一課會繼續分析多位元控制訊號的來源與使用方式。
本課先省略以下細節。讀者可依產品需求再深入。
- 拍內脈衝、X 狀態與亞穩態。
- 綜合後的邏輯、佈局與共同失效。
- Clock/reset 與除錯入口的故障。
- 錯誤後的復原流程與服務可用性。
- 實體攻擊校準與側通道洩漏。
MY ACADEMY · LESSON FILM
教學影片
影片依序說明本課的資料路徑。看完一段,可以回到下面的互動練習,改變輸入或故障條件。動畫呈現教學模型;它沒有替代 RTL 模擬。
旁白使用合成聲音。互動教學與動畫均有模型邊界;請以本課的來源與驗證範圍解讀結果。
MY ACADEMY · RTL LAB
操作碼字:合法值如何變成錯誤授權?
先選 parity,翻轉 bit 0 與 bit 4。看看 00000 如何變成合法的 10001。改用互補編碼翻轉兩個 bit,再用 ECC 修正後繼續的 0x07 範例,觀察誤修正。
位元從右往左編號,bit 0 是最低位。一次事件只能選一個 target。來源或 final grant 故障會清除儲存 mask,分開測試保護邊界。
證據範圍:既有 Python 練習的有限雙態教學模型,觀察 edge 0~7。獨立 reference、clock/reset、取樣端維持可信。沒有執行 RTL/形式/晶片驗證。
SECDED 使用本課自訂的 extended Hamming (8,4)。CE 是解碼器的分類,不保證實際只翻轉一個 bit。錯誤超出模型時,解碼器可能誤修正。
當拍取樣前
當拍更新後
逐拍紀錄(只顯示已走過的拍)
| edge | code Q | decoded | CE / UE | grant | commit | 越權 |
|---|
遷移練習:合法碼字能否證明來源授權?用 source 與 final grant 的獨立案例,找出只保護 register 的缺口。
Wrap-up|把這一課帶回設計審查
- 威脅模型與成立條件
目標是阻止未授權取指。主要實驗只翻轉保存的碼字。每次只有一個事件與一個目標。各組分別限定翻轉位元數。故障在 edge 3 更新後作用。兩次請求在 edge 4、6 到達。觀察期限到 edge 7。
檢查與阻擋電路先保持可信。Clock/reset、完成旗標及握手也不受擾。獨立 reference 保存原本的授權。這些都是實驗假設。它們不是實體隔離的證明。
擴大範圍的實驗分開執行。來源故障只在 edge 2 翻轉來源。最終 grant 故障只在 edge 4 作用。這兩組都不再注入儲存故障。其他可信條件沿用主模型。
- 失效原因
故障可能把合法失敗碼字改成合法通過碼字。Parity 的兩位元反例會漏報。互補編碼的兩位元反例也會漏報。Hamming 的三位元故障會觸發 CE。解碼器卻把它誤修正成通過。
只看 sticky 也有時間缺口。第一個請求可能早於旗標更新。來源若先錯,編碼器會保存合法的錯誤值。最終 grant 若受擾,儲存檢查也無法代替接受端保護。
- 防護方法
資料與檢查位元要一起保存。讀取端要檢查保存值。放行也要完整比對通過碼字。當下錯誤必須直接參與阻擋。Sticky 用來記住錯誤歷史。
授權結果可選擇遇錯即拒絕。本課版本拒絕 CE 與 UE。它不使用修正值放行。這能擋住指定的三位元反例。四位元合法碼字替換仍會越權。來源與最終放行路徑須另行保護。
- 驗證方式與待做檢查
Python 已跑 3,112 個碼字檢查。342 條儲存故障軌跡中有 8 條越權。另有 8 條無故障控制。23 條授權故障案例檢查可用性。來源與最終 grant 各跑 4 條。當拍阻擋與 sticky 延遲也有對照。
尚未執行 RTL 模擬或形式證明。綜合與矽上測試也尚未執行。後續環境須限制注入預算。它也要檢查接受時機及正常可用性。網站圖解驗收不是硬體驗證。
- 防護界線與未驗證項目
這是有限的兩態取樣模型。它沒有拍內脈衝、X 或亞穩態。它也沒有傳播延遲與佈局效應。8/342 不是實體攻擊成功率。窗口內沒有越權,也不是永久安全。
多個暫存器可能同時受擾。檢查電路與來源也可能被攻擊。綜合可能合併冗餘邏輯。這次沒有驗證這些實體邊界。重複注入、復原與側通道也未涵蓋。
換個情境再想一次
把故障預算從一位元改成三位元。先預測修正後繼續是否仍安全。再重跑 mask 0x07。接著把來源加入目標範圍。請說明為何合法碼字仍可能越權。最後,寫出新的可信邊界與接受期限。
以上整理對照本課的教學案例、參考資料與實驗範圍;未列為已完成的驗證,都是後續工作。
學習指南
RTL Anti-Tampering Design|RTL 防竄改設計
查看課程大綱 → · 進度只計入已發布課程
先備知識
- 先認識 0 與 1;第二課可協助理解故障模型
我學會了什麼
- 區分合法碼字與正確授權
- 比較 parity、互補編碼與 SECDED
- 在接受取指前阻擋錯誤
- 區分修正、安全與可用性