WEBVTT

1
00:00:00.600 --> 00:00:02.780
簽章失敗，結果暫存器存零。

2
00:00:02.780 --> 00:00:10.480
畫面在 edge 三把讀取值短暫翻成一，edge 四才來取指請求，此時已經恢復零。

3
00:00:10.480 --> 00:00:14.260
沒有越權，但這裡沒有 detector，談不上偵測成功。

4
00:00:14.260 --> 00:00:20.660
先把正常排程固定：edge 零 reset，edge 二驗證完成，edge 四和六各有

5
00:00:20.660 --> 00:00:23.780
一筆有效且 ready 的請求，觀察到 edge 七。

6
00:00:23.780 --> 00:00:27.340
兩筆屬於同一次開機，合用一個故障預算。

7
00:00:27.800 --> 00:00:32.400
checked_q 記錄驗證完成，result_q 保存是否通過。

8
00:00:32.400 --> 00:00:36.020
grant 用 checked 和讀取到的 result 做 AND。

9
00:00:36.020 --> 00:00:40.340
取指 valid、接收端 ready 與 grant 在上升緣都為一，才記

10
00:00:40.340 --> 00:00:42.100
accepted_commit。

11
00:00:42.100 --> 00:00:46.420
這是簡化取指交付，不是指令已經執行或退休。

12
00:00:46.420 --> 00:00:51.420
接下來改的是 grant 上游看見的值，最後仍要到這個緣查結果。

13
00:00:52.000 --> 00:00:53.760
把兩條線拆開。

14
00:00:53.760 --> 00:01:00.840
A 只把下游當下看到的 Q 反相，控制消失就恢復；暫存器原值沒有變。

15
00:01:00.840 --> 00:01:05.760
B 改的是保存狀態，控制消失後，下一次讀取還是錯的。

16
00:01:05.760 --> 00:01:10.000
它們都可能被叫 bit flip，但需要不同恢復條件。

17
00:01:10.000 --> 00:01:14.210
位置、持續時間與取樣時刻，才決定後面請求讀到什麼。

18
00:01:15.020 --> 00:01:19.860
模型卡先寫要保護的事件：未授權映像不能取得取指接受。

19
00:01:19.860 --> 00:01:23.960
接著放初始狀態、請求排程與期限。

20
00:01:23.960 --> 00:01:29.480
以 B 為例，target 是保存的 result，效果是反相一次，留到正常覆寫或

21
00:01:29.480 --> 00:01:32.660
reset；沒有一直強制成一。

22
00:01:32.660 --> 00:01:37.260
同事照這張卡設定注入器，應該能重跑同一條軌跡。

23
00:01:37.260 --> 00:01:40.420
若 target 改成 clock 或 checker，就另寫一張卡。

24
00:01:41.060 --> 00:01:44.780
每個 edge 先讀舊 Q、grant，記接受事件。

25
00:01:44.780 --> 00:01:49.260
再做正常暫存器更新，最後把 B 的反相加到新狀態。

26
00:01:49.260 --> 00:01:55.440
edge 三後翻轉，會改 edge 四讀到的值，不會回去改 edge 三已記錄的事件。

27
00:01:55.440 --> 00:02:00.020
把這個順序畫出來，才不會把更新後的 Q 拿來解釋更新前的接受。

28
00:02:00.560 --> 00:02:05.260
一次事件、單一位置與單一位元，各自限制不同事情。

29
00:02:05.260 --> 00:02:10.320
edge 三翻一次，保存值可以讓 edge 四和六都越權，仍是一次事件。

30
00:02:10.320 --> 00:02:14.220
edge 三和五各翻一次，就超出預算，即使是同一個 bit。

31
00:02:14.220 --> 00:02:18.420
這份預算涵蓋 reset 到 edge 七，下一次 reset 才重開。

32
00:02:18.420 --> 00:02:23.500
裝置一生能重試幾次，產品還要另外限制，不能從 per attempt 推成永久安全。

33
00:02:24.540 --> 00:02:27.360
映像、政策與獨立 reference 先保持可信。

34
00:02:27.360 --> 00:02:32.620
clock、reset、完成訊號、checked、非 target 邏輯與接受機制也不受擾。

35
00:02:32.620 --> 00:02:37.000
reference 保留原來失敗的判斷，不能從受攻擊的 result 複製。

36
00:02:37.000 --> 00:02:41.640
這些排除讓小模型能隔離原因，沒有證明它們在真實產品都打不到。

37
00:02:42.100 --> 00:02:44.940
A 在讀取路徑加測試 XOR。

38
00:02:44.940 --> 00:02:48.600
控制是一，下游看到反相；回零又讀原 Q。

39
00:02:48.600 --> 00:02:52.280
只要這條觀察線沒有回授到 D，就不會改保存值。

40
00:02:52.280 --> 00:02:56.700
原排程的短脈衝在 edge 三結束，edge 四讀到零，因此沒有接受。

41
00:02:56.700 --> 00:02:59.900
把同一脈衝移到請求緣，結果就可能改變。

42
00:02:59.900 --> 00:03:02.080
這裡是錯過取樣，沒有主動防護。

43
00:03:02.560 --> 00:03:06.560
B 先選正常 next state，再 XOR 一次存進 DFF。

44
00:03:06.560 --> 00:03:09.280
edge 三更新後，失敗零變成一。

45
00:03:09.280 --> 00:03:14.420
下一拍控制回零，但 hold 路徑繼續讀這個一，所以 edge 四與六都接受。

46
00:03:14.420 --> 00:03:17.640
兩筆越權來自同一事件，沒有每拍重打。

47
00:03:17.640 --> 00:03:22.540
這個 RTL 形式描述保存效果，還沒有證明雷射或電磁真的耦合到實體 D 端。

48
00:03:23.340 --> 00:03:26.520
C 把編碼前的 auth_ok 讀成反相。

49
00:03:26.520 --> 00:03:32.020
涵蓋 edge 二驗證完成的緣，就把錯答案存進 result，脈衝結束也不會恢復。

50
00:03:32.020 --> 00:03:35.160
若只在 edge 三作用，edge 二早已寫完，checked 也關掉 write

51
00:03:35.160 --> 00:03:36.320
enable，result 不變。

52
00:03:36.320 --> 00:03:39.880
要一起讀 verify_done、checked 和實際寫入條件。

53
00:03:39.880 --> 00:03:43.320
C 與 B 是各自的軌跡，沒有同時打來源和儲存。

54
00:03:43.643 --> 00:03:49.443
真正 RTL testbench 的控制要在取樣緣前穩定，觀察也要分更新前後。

55
00:03:49.443 --> 00:03:53.083
如果在 posedge 同時用 blocking assignment 改注入控制，

56
00:03:53.083 --> 00:03:55.763
DUT 與 monitor 可能讀到不同順序。

57
00:03:55.763 --> 00:04:00.863
這個 Python 模型沒有模擬事件區域競爭，也沒有拍內 glitch 或亞穩態。

58
00:04:00.863 --> 00:04:03.703
換成 simulator 時，還要另外處理這些行為。

59
00:04:04.303 --> 00:04:08.263
force、release、backdoor deposit 或注入 mux，只說用了

60
00:04:08.263 --> 00:04:13.123
哪種工具，還要看 simulator 怎麼處理 net、variable 與正常更新。

61
00:04:13.123 --> 00:04:18.883
圖裡 fi 用來重現指定故障，沒有提供保護功能，正式產品應移除。

62
00:04:18.883 --> 00:04:25.563
實驗紀錄要寫出 target、效果和恢復方式，光是 API 名稱還不能讓同事重跑相同結果。

63
00:04:25.563 --> 00:04:30.163
另開一條 D 軌跡，edge 四把最末 grant 的零翻成一。

64
00:04:30.163 --> 00:04:33.683
上游仍是正確失敗，下游這次卻能接受。

65
00:04:33.683 --> 00:04:37.803
A、B、C 原本沒攻擊這裡，所以結論不能搬過來。

66
00:04:37.803 --> 00:04:42.463
D 的握手和真正接受機制仍可信，也沒有檢查 consumer 裡每個節點。

67
00:04:42.463 --> 00:04:45.203
新增 target，可信邊界就跟著變。

68
00:04:45.663 --> 00:04:51.303
每次 accepted_commit，都要在同一取樣緣符合獨立 reference 的完成與通過。

69
00:04:51.303 --> 00:04:53.503
事後 alert 不能替代這個條件。

70
00:04:53.503 --> 00:04:58.183
reset 有效時排除檢查，故障預算由 harness 實際限制。

71
00:04:58.183 --> 00:05:04.743
教材有 assertion 範例，可放進後續驗證環境；這段動畫沒有聲稱已編譯或完成形式證明。

72
00:05:05.123 --> 00:05:08.103
換成合法映像，應該能到取指接受。

73
00:05:08.103 --> 00:05:12.503
cover 可以找出可達路徑，不能保證每次正常開機都走到。

74
00:05:12.503 --> 00:05:15.643
還得寫進度、timeout 與復原需求。

75
00:05:15.643 --> 00:05:20.783
永遠禁止取指，可能滿足剛才的窄安全性質，卻不能讓裝置工作。

76
00:05:20.783 --> 00:05:22.323
這兩類結果要分開回報。

77
00:05:22.643 --> 00:05:25.483
起點選 edge 二到七，共六個。

78
00:05:25.483 --> 00:05:31.523
A、C、D 各測一緣或兩緣脈衝，B 每個起點反相一次，合成四十二個 fault

79
00:05:31.523 --> 00:05:34.343
case，另有兩個無故障控制。

80
00:05:34.343 --> 00:05:38.643
每條獨立 reset，用同樣失敗映像和請求。

81
00:05:38.643 --> 00:05:42.843
原 Python 枚舉十八條有越權，二十四條窗口內沒有。

82
00:05:42.843 --> 00:05:47.763
PASS 只是重現預期，連刻意脆弱的越權也在裡面。

83
00:05:47.763 --> 00:05:52.603
十八除以四十二沒有量測機率、強度或位置可達性，不能當實體成功率。

84
00:05:53.103 --> 00:05:59.243
B 若在 edge 六更新後才翻轉，原本最後一筆請求已經取樣，窗口內就看不到越權。

85
00:05:59.243 --> 00:06:03.983
把 edge 七也加一筆請求，保存的一就會被用到，這次能接受。

86
00:06:03.983 --> 00:06:06.623
前一輪沒有測這個機會。

87
00:06:06.623 --> 00:06:12.863
比較防護之前，先把工作負載列入條件，否則相同錯值可以得到兩種看似矛盾的結果。

88
00:06:13.783 --> 00:06:20.303
紀錄設計和模型版本、target、注入設定、初始狀態、請求、期限與反例 trace。

89
00:06:20.303 --> 00:06:25.603
先查注入有沒有生效，再查敏感請求有沒有到，最後查性質有沒有執行。

90
00:06:25.603 --> 00:06:32.103
敏感請求沒到、timeout、注入失敗或 assertion 關掉，都留成未判定，不能歸到安全通過。

91
00:06:32.103 --> 00:06:34.663
重跑紀錄需要保存這些差別。

92
00:06:35.243 --> 00:06:41.403
讀 SYNFI、VerFI 或 FIRMER，先對位置、效果、事件計數、時間與觀察點。

93
00:06:41.403 --> 00:06:46.923
netlist 分析、SAT 證明與這裡逐 edge 的程式，假設未必相同。

94
00:06:46.923 --> 00:06:53.343
這課沒有執行那些工具，也沒有重現 benchmark；不能把各自的數字湊成同一個防護保證。

95
00:06:53.343 --> 00:06:59.623
產品可能有 prefetch、DMA、debug 或 key 讀取，各自要找敏感交付事件。

96
00:06:59.623 --> 00:07:06.203
RTL target 到 netlist 要核對位置，接實體測試還要校準效果，阻擋也得早於接受。

97
00:07:06.203 --> 00:07:11.383
clock、reset、多位元、反覆注入和資訊洩漏，都要另外建模型。

98
00:07:11.383 --> 00:07:15.483
這份結果只看一次嘗試到 edge 七，還沒涵蓋那些情況。

99
00:07:15.893 --> 00:07:20.553
把 edge 六後的 B 翻轉寫進模型卡，先用原請求，再加 edge 七。

100
00:07:20.553 --> 00:07:28.473
兩次都寫清 target、效果、預算、可信部分與期限，分別報接受、偵測和及時阻擋。

101
00:07:28.473 --> 00:07:33.473
這樣同事能核對，是工作負載改變了結果，還是防護真的介入。

102
00:07:33.473 --> 00:07:37.613
下一課比較保存編碼時，也沿用這份接受點與實驗條件。

