WEBVTT

1
00:00:00.000 --> 00:00:02.180
這份韌體的簽章沒有通過。

2
00:00:02.180 --> 00:00:07.160
驗證器把失敗的零寫進暫存器，處理器本來應該等著。

3
00:00:07.160 --> 00:00:10.260
現在只改一件事：把保存的零翻成一。

4
00:00:10.260 --> 00:00:14.880
驗證器沒有重新算，簽章也沒有改變，授權卻可能打開。

5
00:00:14.880 --> 00:00:20.220
沿著畫面追下去，判斷要經過保存、授權邏輯，再到取指介面。

6
00:00:20.220 --> 00:00:22.700
這幾站都會影響程式能不能開始跑。

7
00:00:23.300 --> 00:00:26.160
取指是處理器讀取程式指令。

8
00:00:26.160 --> 00:00:33.780
這裡先用簡化介面：valid 表示有請求，ready 表示接收端能收，grant 表示允許交付。

9
00:00:33.780 --> 00:00:37.760
三個值都在約定的上升緣成立，才算接受一筆取指。

10
00:00:37.760 --> 00:00:41.020
指令接著怎麼執行、何時退休，不在這個事件裡。

11
00:00:41.020 --> 00:00:45.660
畫面是教學模型，沒有跑完整 CPU 的 RTL，也沒有量測晶片。

12
00:00:46.080 --> 00:00:48.300
暫存器裡有兩個旗標。

13
00:00:48.300 --> 00:00:53.100
checked_q 記錄檢查已完成，verified_q 記錄是否通過。

14
00:00:53.100 --> 00:00:58.500
這次簽章失敗，檢查仍然完成了，所以是 checked 為一、verified 為零。

15
00:00:58.500 --> 00:01:01.580
檢查做完了，失敗答案仍然不能放行。

16
00:01:01.580 --> 00:01:07.420
reset 開始新的開機嘗試；這個例子只看單一時脈域，也還沒包含完整的開機控制器。

17
00:01:08.316 --> 00:01:10.980
checked 變成一後，正常寫入就停止。

18
00:01:10.980 --> 00:01:14.780
暫存器把 verified 的零留住，grant 還是一直讀它。

19
00:01:14.780 --> 00:01:20.680
若保存狀態在這時受擾，下游會讀到改過的值；並不需要再來一次正常寫入。

20
00:01:20.680 --> 00:01:24.080
注意畫面上關掉的是寫入致能，沒有關掉讀取路徑。

21
00:01:24.640 --> 00:01:26.308
先看故障前。

22
00:01:26.308 --> 00:01:30.740
checked 是一，verified 是零，兩者做 AND，grant 就是零。

23
00:01:30.740 --> 00:01:35.640
把 verified 翻成一，AND 的兩個輸入現在都成立，grant 升高。

24
00:01:35.640 --> 00:01:37.980
接著有有效且 ready 的請求，

25
00:01:37.980 --> 00:01:39.740
到了取樣緣就會接受。

26
00:01:39.740 --> 00:01:43.800
獨立觀察器記得原來簽章失敗，這筆取指因此是未授權的。

27
00:01:44.125 --> 00:01:48.205
這次只允許在結果保存後，翻轉結果暫存器的一個位元。

28
00:01:48.205 --> 00:01:53.925
一次開機嘗試，最多一個事件、一個位置；改過的值留到覆寫或 reset。

29
00:01:53.925 --> 00:01:59.525
一次事件可以造成後面好幾筆錯誤交付，預算沒有因此重新開始。

30
00:01:59.525 --> 00:02:03.225
這個限定讓反例可以重跑，也限制了它能回答的問題。

31
00:02:03.785 --> 00:02:10.265
這個實驗把驗證器、獨立觀察器、clock、reset、grant 閘與接收介面先列為可信。

32
00:02:10.265 --> 00:02:12.225
只攻擊結果暫存器。

33
00:02:12.225 --> 00:02:17.705
從 reset 解除開始觀察，到第一筆取指或預先設定的期限結束。

34
00:02:17.705 --> 00:02:23.105
若換成攻擊比較器、最末 grant，或同時改多處，就要重跑新的模型。

35
00:02:23.105 --> 00:02:25.225
原本的結果沒有涵蓋新增的位置。

36
00:02:25.985 --> 00:02:29.505
畫面直接把零改成一，是邏輯故障模型。

37
00:02:29.505 --> 00:02:34.625
電壓、clock、電磁與雷射擾動，各有實際作用位置與持續時間。

38
00:02:34.625 --> 00:02:38.525
要把它們連到這個位元翻轉，需要量測和時序分析。

39
00:02:38.525 --> 00:02:44.685
這裡重現的是假設下的錯誤路徑，還沒有證明某種物理方法會在晶片上造成相同效果。

40
00:02:44.685 --> 00:02:47.645
把同一條授權路徑畫成狀態機。

41
00:02:47.645 --> 00:02:51.285
WAIT 到 CHECK，檢查後應該去 ERROR；成功才去 RELEASE。

42
00:02:51.285 --> 00:02:56.845
若故障把選路條件改成成功，機器可能沿著已有的邊走進 RELEASE。

43
00:02:56.845 --> 00:03:00.765
RELEASE 的編碼本來就合法，所以非法狀態檢查不會報錯。

44
00:03:00.765 --> 00:03:04.605
要判斷這次轉移能不能放行，還得查驗證證據。

45
00:03:05.225 --> 00:03:07.685
CHECK 到 RELEASE 這條邊也可能合法。

46
00:03:07.685 --> 00:03:10.365
問題是這次用了什麼條件。

47
00:03:10.365 --> 00:03:14.925
要查目前狀態、選路條件，還有之前真的完成了哪些工作。

48
00:03:14.925 --> 00:03:20.885
算出摘要，只證明摘要計算完成；簽章驗證還需要自己的完成與通過證據。

49
00:03:20.885 --> 00:03:25.425
只驗圖上有這條邊，或多加一次合法碼檢查，都回答不了這件事。

50
00:03:25.765 --> 00:03:28.925
回到介面，三個訊號要一起取樣。

51
00:03:28.925 --> 00:03:34.465
valid 和 ready 都是一，只表示這筆請求有交付機會，還要 grant。

52
00:03:34.465 --> 00:03:37.445
accepted_commit 記錄的就是這個上升緣。

53
00:03:37.445 --> 00:03:42.345
安全檢查在同一緣問：這份映像真的完成驗證並通過了嗎？

54
00:03:42.345 --> 00:03:46.325
只盯某個旗標有沒有動，可能漏掉實際已經交出去的取指。

55
00:03:46.845 --> 00:03:54.825
看這個示意順序：t 發生故障，t 加一接受取指，t 加二才報警，t 加五才 reset。

56
00:03:54.825 --> 00:03:58.505
這些間隔沒有量測產品，只用來分清先後。

57
00:03:58.505 --> 00:04:04.645
若測試只要求最後有警報，這次仍可能通過，但未授權取指已經發生。

58
00:04:04.645 --> 00:04:09.745
警報可以回報和協助復原；那筆接受事件無法撤回。

59
00:04:09.745 --> 00:04:12.505
阻擋與通報因此要各自設定觀察點和期限。

60
00:04:13.105 --> 00:04:18.165
本地阻擋必須在下一個可能接受的緣之前，把錯誤授權壓下來。

61
00:04:18.165 --> 00:04:21.385
警報後續負責回報、升級或清理。

62
00:04:21.385 --> 00:04:29.005
產品還要找出其他交付路徑：預取可能先拿走指令，DMA 可以搬資料，debug 也可能取得權限。

63
00:04:29.005 --> 00:04:32.945
只守住 CPU reset，沒有自動守住這些接受事件。

64
00:04:33.365 --> 00:04:35.585
現在把結果改成四位元。

65
00:04:35.585 --> 00:04:42.185
真用零一一零，假用一零零一，四個位置全部不同，漢明距離是四。

66
00:04:42.185 --> 00:04:44.865
接收端要完整比對零一一零。

67
00:04:44.865 --> 00:04:51.145
若只看某一位，或把任何非零值都當成真，新增的位元就沒有用在這個授權判斷上。

68
00:04:51.565 --> 00:04:55.185
從一零零一出發，翻一位有四種結果。

69
00:04:55.185 --> 00:04:59.765
畫面把它們各自和真碼字比對，都不相等，因此拒絕。

70
00:04:59.765 --> 00:05:02.985
這個檢查限定二態輸入與單一翻轉預算。

71
00:05:02.985 --> 00:05:09.425
它證明這幾種保存改動不會被當成真，沒有涵蓋所有故障，也沒有證明整顆晶片安全。

72
00:05:09.932 --> 00:05:12.272
把 target 往前移到編碼器的輸入。

73
00:05:12.272 --> 00:05:17.672
原本失敗的判斷被改成成功，編碼器會正常產生零一一零。

74
00:05:17.672 --> 00:05:22.452
碼字合法，下游也完整比對成功，卻放了沒有授權的映像。

75
00:05:22.452 --> 00:05:28.272
完整碼字可以限制指定的保存故障；答案來源仍需要另外的證據。

76
00:05:28.892 --> 00:05:34.892
較完整的 grant 要求檢查完成、完整真碼字、目前階段允許，而且沒有本地故障。

77
00:05:34.892 --> 00:05:37.352
每個條件都得有可信來源。

78
00:05:37.352 --> 00:05:43.272
比較器與最末 grant 閘也會影響結果，不能因為條件變多就略過它們。

79
00:05:43.272 --> 00:05:48.892
這段邏輯定義的是消費端契約，後面還要設計防護與完整 reset 控制。

80
00:05:48.892 --> 00:05:53.292
觀察器獨立記錄這份映像是否完成驗證並通過。

81
00:05:53.292 --> 00:05:58.352
設計接受取指時，觀察器若仍記著失敗，安全性檢查就報錯。

82
00:05:58.352 --> 00:06:04.732
若把受攻擊的 verified 直接複製過去，兩邊會一起變一，矛盾反而被藏起來。

83
00:06:04.732 --> 00:06:08.052
獨立參考必須避開正在檢查的故障路徑。

84
00:06:08.052 --> 00:06:13.332
原課程的有限模型檢查十六個碼字、四個單一翻轉和六個情境。

85
00:06:13.332 --> 00:06:18.912
預期結果裡包含有漏洞設計的成功繞過；重現這些結果也會印出 PASS。

86
00:06:18.912 --> 00:06:23.352
這裡沒有執行 RTL 模擬、形式證明或晶片實測。

87
00:06:23.352 --> 00:06:29.752
看紀錄時，要一起看每個案例預期的是拒絕還是越權，不能只讀最後那個字。

88
00:06:29.752 --> 00:06:34.232
再換成合法映像，先不加故障，確認它能取得取指。

89
00:06:34.232 --> 00:06:40.112
永久把 grant 拉低，前面的拒絕檢查可能都會通過，開機卻永遠走不下去。

90
00:06:40.112 --> 00:06:42.992
因此要留下正常工作可達的證據。

91
00:06:42.992 --> 00:06:49.212
cover 可以顯示有這條路徑；每次都能完成的完整活性要求，仍要另外證明。

92
00:06:49.532 --> 00:06:56.372
在自己的設計挑一筆真正交出權限的事件，往前追到判斷來源、保存值和消費端。

93
00:06:56.372 --> 00:07:02.432
記下這次可以改哪裡，其他哪些部分可信，以及阻擋必須何時到達。

94
00:07:02.432 --> 00:07:05.112
現在把最末 grant 閘也列為 target。

95
00:07:05.112 --> 00:07:08.792
原本的四位元保護還能阻止那筆交付嗎？

96
00:07:08.792 --> 00:07:10.532
用新的邊界重找反例。