WEBVTT

1
00:00:00.000 --> 00:00:03.380
驗證失敗時存零，翻成一卻會放行。

2
00:00:03.380 --> 00:00:07.820
單一 bit 的兩個值都合法，讀取端沒有非法格式可以辨認。

3
00:00:07.820 --> 00:00:13.220
多存檢查位元，可以讓某些改動走到非法組合，再趕在使用前阻擋。

4
00:00:13.220 --> 00:00:17.480
但合法失敗若變成合法通過，格式檢查仍會接受。

5
00:00:17.480 --> 00:00:24.080
這次沿同一筆取指，比較 parity、兩位元互補碼與錯誤修正碼，看各自抓得到哪些改動。

6
00:00:24.540 --> 00:00:30.060
主實驗每條軌跡只攻擊一個保存碼字，一次事件，分組翻一到四 bits。

7
00:00:30.060 --> 00:00:36.840
edge 三更新後改值，留到後面，edge 四和六有有效且 ready 的請求，觀察到七。

8
00:00:36.840 --> 00:00:43.580
編碼、檢查、阻擋、錯誤歷史、完成旗標先可信；映像、政策、獨立 reference、

9
00:00:43.580 --> 00:00:47.080
clock、reset、握手與接受機制也不受擾。

10
00:00:47.080 --> 00:00:49.200
reference 不讀故障碼字。

11
00:00:49.200 --> 00:00:53.220
這些是模型假設，產品還要驗證物理擾動是否跨越它們。

12
00:00:53.720 --> 00:00:58.200
四個 data bits 旁邊存一個 parity，五位裡一的數量要是偶數。

13
00:00:58.200 --> 00:01:04.060
資料零零零零表示失敗，零零零一表示通過；其他資料不能放行。

14
00:01:04.060 --> 00:01:09.900
畫面從高位的 parity 接到四位資料，失敗是五個零，通過是一零零零一。

15
00:01:09.900 --> 00:01:13.700
parity 留的是寫入時的檢查值，讀取時才有東西對照。

16
00:01:14.400 --> 00:01:18.120
五個零翻任何一位，奇偶都變了，local_bad 就是一。

17
00:01:18.120 --> 00:01:21.880
這抓得到任一單一保存翻轉，但不知道錯在哪一位。

18
00:01:21.880 --> 00:01:26.900
grant 還要完整比對通過資料，並直接用當下 local_bad 阻擋。

19
00:01:26.900 --> 00:01:33.900
注意不能從已改壞的資料重算 parity，再自己比自己；兩者會永遠相符，沒有檢查保存期間的變化。

20
00:01:34.360 --> 00:01:37.440
現在同時翻 data 的最低位與 parity。

21
00:01:37.440 --> 00:01:42.880
五個零變成一零零零一，一的數量仍是偶數，data 也正好是通過值。

22
00:01:42.880 --> 00:01:46.640
這個 mask 是十六進位一一，沒有 parity 警報。

23
00:01:46.640 --> 00:01:52.720
它給出一個兩位反例；其他兩位改動未必讓 data 變成通過，不能都算成同一結果。

24
00:01:53.083 --> 00:01:55.263
換成兩個保存位元。

25
00:01:55.263 --> 00:01:59.803
零一表示失敗，一零表示通過，零零與一一非法。

26
00:01:59.803 --> 00:02:03.323
讀取端先查兩位互補，再完整比對一零。

27
00:02:03.323 --> 00:02:08.843
這次多存一位，把單一翻轉留下非法組合，接收端才有可拒絕的格式。

28
00:02:09.683 --> 00:02:13.123
零一翻一位變零零或一一，可以拒絕。

29
00:02:13.123 --> 00:02:19.643
兩位一起翻，mask 零三，直接變一零，互補關係仍成立，卻已經錯放行。

30
00:02:19.643 --> 00:02:22.283
兩份值也不代表簽章驗了兩次。

31
00:02:22.283 --> 00:02:28.923
如果只有一個 Q，讀取端即時做 NOT，Q 變動時反值跟著變，永遠互補。

32
00:02:28.923 --> 00:02:33.423
要檢查保存改動，反值得在可信寫入時產生，兩邊各自存。

33
00:02:34.243 --> 00:02:36.803
這裡 ECC 指錯誤修正碼。

34
00:02:36.803 --> 00:02:44.123
SECDED 在設計範圍內修正單 bit、偵測雙 bit，更多 bits 不能直接照這個承諾推。

35
00:02:44.123 --> 00:02:48.763
例子用自訂 extended Hamming 八四碼，四位資料加四位檢查。

36
00:02:48.763 --> 00:02:52.643
它不是橢圓曲線密碼，也不是 OpenTitan 所有核心共用的編碼。

37
00:02:53.423 --> 00:02:58.443
位置一、二、四、八放檢查位，三、五、六、七放四位資料。

38
00:02:58.443 --> 00:03:04.143
一到八對應儲存 bit 零到七，二進位顯示則反過來從七到零。

39
00:03:04.143 --> 00:03:08.803
這個配置把失敗編成十六進位零零，通過編成八七。

40
00:03:08.803 --> 00:03:12.863
等一下翻的位置，都用這張表對，不能把顯示左邊誤當位置一。

41
00:03:13.563 --> 00:03:16.143
解碼器看 syndrome 與整體 parity。

42
00:03:16.143 --> 00:03:18.003
兩者零，不報錯。

43
00:03:18.003 --> 00:03:23.623
syndrome 零、parity 一，翻位置八；兩者非零，翻 syndrome 指的位置。

44
00:03:23.623 --> 00:03:27.423
syndrome 非零但 parity 零，報 UE，不可修正。

45
00:03:27.423 --> 00:03:29.883
前兩種修正情況報 CE。

46
00:03:29.883 --> 00:03:33.923
這些旗標分類的是收到的碼字，沒有量到剛才實際翻了幾位。

47
00:03:34.292 --> 00:03:37.332
從零零翻位置一、二、三，

48
00:03:37.332 --> 00:03:38.592
得到零七。

49
00:03:38.592 --> 00:03:42.532
三個索引 XOR 抵消，syndrome 是零，整體 parity 卻是一。

50
00:03:42.532 --> 00:03:46.252
解碼器按剛才的表報 CE，認為位置八錯了。

51
00:03:46.252 --> 00:03:50.452
它接著翻位置八，零七變八七，正好是合法通過。

52
00:03:50.452 --> 00:03:52.952
這個三位 pattern 被誤修正了。

53
00:03:52.952 --> 00:03:56.512
其他三位組合要各自算，不能都套成同樣結果。

54
00:03:56.512 --> 00:04:01.512
修正後繼續，grant 用 corrected data，只在 UE 拒絕。

55
00:04:01.512 --> 00:04:05.012
剛才零七報 CE，修成八七後就會越權。

56
00:04:05.012 --> 00:04:08.492
CE 沒有證明實際只壞一位，它只是解碼器的分類。

57
00:04:08.492 --> 00:04:13.052
授權資料要把超出單位修正範圍的這條路，也追到接受事件。

58
00:04:13.832 --> 00:04:18.392
遇錯即拒絕，用 CE 或 UE 直接阻擋，不拿修正值放行。

59
00:04:18.392 --> 00:04:20.512
零七的三位反例在這裡被擋住。

60
00:04:20.512 --> 00:04:23.192
再把故障改成 mask 八七，

61
00:04:23.192 --> 00:04:24.672
翻四個指定 bits，

62
00:04:24.672 --> 00:04:28.032
零零直接變合法八七，syndrome 和 parity 都正常。

63
00:04:28.032 --> 00:04:31.952
這次政策沒有錯誤旗標可用，仍可能越權。

64
00:04:31.952 --> 00:04:33.832
更改政策後，碼距限制還在。

65
00:04:34.392 --> 00:04:37.912
local_bad 是當下錯誤，sticky 記錄曾經報錯。

66
00:04:37.912 --> 00:04:43.412
edge 三後改壞碼字，edge 四前 local_bad 已是一，但舊 sticky 還是零。

67
00:04:43.412 --> 00:04:47.112
只查 sticky 的接收端會先接受，再把歷史設一。

68
00:04:47.112 --> 00:04:51.952
grant 要同時查完成、完整通過值、當下無錯與沒有歷史錯誤。

69
00:04:51.952 --> 00:04:57.092
當下阻擋才能趕上第一筆；真正產品還要證明傳播路徑在接受緣前穩定。

70
00:04:57.092 --> 00:05:01.152
主表裡錯誤一直保留，偵測到的 local_bad 也一直成立。

71
00:05:01.152 --> 00:05:04.332
這些案例沒有另外證明 sticky 多擋了什麼。

72
00:05:04.332 --> 00:05:09.752
若異常消失，或值被正常覆寫，留下歷史是另一個用途，需要新增測試。

73
00:05:09.752 --> 00:05:12.652
這裡先只回報主表真正跑過的持續情境。

74
00:05:12.972 --> 00:05:17.832
把 parity 一一、互補零三、Hamming 零七三個 masks 放一起。

75
00:05:17.832 --> 00:05:22.972
前兩者直接換成合法通過，第三者透過誤修正到通過。

76
00:05:22.972 --> 00:05:30.512
每條都先看 edge 三後存了什麼，再看 edge 四前旗標，最後看 grant 選原值還是修正值。

77
00:05:30.512 --> 00:05:34.572
用相同接受點，才能解釋編碼和政策的差別。

78
00:05:35.172 --> 00:05:39.332
原主表有三百四十二條儲存故障軌跡，八條越權。

79
00:05:39.332 --> 00:05:43.172
parity 兩位一條，互補兩位一條。

80
00:05:43.172 --> 00:05:49.472
修正後繼續，三位四條、四位一條；遇錯即拒絕，四位一條。

81
00:05:49.472 --> 00:05:51.532
每個 mask 算一條軌跡。

82
00:05:51.532 --> 00:05:55.092
它造成兩筆接受，軌跡數仍然是一。

83
00:05:55.092 --> 00:06:00.492
這些是有限二態模型和固定請求的結果，沒有量測攻擊成功機率。

84
00:06:01.492 --> 00:06:05.812
碼字檢查另有三千一百一十二個，不要混成取指 trace。

85
00:06:05.812 --> 00:06:11.192
再看八條無故障控制和二十三條合法映像的單 bit 故障。

86
00:06:11.192 --> 00:06:14.632
八條修正後仍能取指，十五條被阻擋。

87
00:06:14.632 --> 00:06:22.032
拒絕政策可以保護授權，卻讓合法工作中斷；安全與可用性因此要一起列出，但各自計數。

88
00:06:22.832 --> 00:06:24.812
另開來源 target 的實驗。

89
00:06:24.812 --> 00:06:32.892
edge 二寫入前，auth_ok 從零改一，編碼器就正常產生通過碼字，四個版本都越權。

90
00:06:32.892 --> 00:06:35.052
沒有同時翻保存值。

91
00:06:35.052 --> 00:06:42.432
這條擴大模型的結果說明，格式不能替來源授權，也不能把答案綁到這份映像與這次交易。

92
00:06:42.432 --> 00:06:44.732
編碼之外還要保護這個判斷來源。

93
00:06:45.412 --> 00:06:47.992
再另開最末 grant 的 target。

94
00:06:47.992 --> 00:06:53.252
edge 四把零改一，上游仍存正確失敗，第一筆取指卻被接受。

95
00:06:53.252 --> 00:06:56.972
四種保存方案都沒有保護這個新增位置。

96
00:06:56.972 --> 00:07:01.252
握手與真正接受機制仍可信，也沒有測 consumer 每一處。

97
00:07:01.252 --> 00:07:04.172
這不是和來源或保存一起打的多位置案例。

98
00:07:04.472 --> 00:07:10.592
實體兩份暫存器可能相鄰，共用來源、clock 或 reset，綜合也可能合併重複邏輯。

99
00:07:10.592 --> 00:07:14.352
要檢查實作結構、局部反應與告警路徑。

100
00:07:14.352 --> 00:07:20.612
OpenTitan 指南提醒這些實作問題；OTBN 使用不同完整性碼與不自動修正政策。

101
00:07:20.612 --> 00:07:24.672
這個自訂 Hamming 例子沒有複製它的碼，也沒有驗證那個產品。

102
00:07:25.132 --> 00:07:30.992
每次接受都要同拍符合獨立 reference 的完成與授權，合法操作也要可達。

103
00:07:30.992 --> 00:07:38.292
SVA 範例還要放進 harness，實際限制事件數、mask 位寬與翻轉數，才能檢查指定的模型。

104
00:07:38.292 --> 00:07:40.772
這些範例還不是已完成的證明。

105
00:07:40.772 --> 00:07:45.292
現在把單 bit 預算改成三 bits，重跑零七那條：continue 和

106
00:07:45.292 --> 00:07:47.292
reject 各用哪份值？

107
00:07:47.292 --> 00:07:48.832
回到接受點查。

108
00:07:48.832 --> 00:07:56.252
X、glitch、延遲、佈局、共同失效、復原與側通道，仍需要後續 RTL 與實體證據；

109
00:07:56.252 --> 00:07:58.732
讀論文也要核對它們的路徑和 bit 預算。