WEBVTT

1
00:00:00.000 --> 00:00:06.440
安全結論要能回答：保護什麼、假設哪些故障、哪些邊界已驗、哪些反例仍成立，

2
00:00:06.440 --> 00:00:13.920
以及未知項在哪裡。證據包的目的不是堆報表，而是讓另一位工程師能重跑並指出結論邊界。

3
00:00:13.920 --> 00:00:16.580
建築驗收不能只交一張「合格」貼紙；

4
00:00:16.580 --> 00:00:20.520
要知道檢查的是哪一層、哪個日期、哪些房間未開放。

5
00:00:20.520 --> 00:00:26.620
硬體安全審查也從可反駁 claim 開始，例如「在最多一個保存旗標 transient upset，

6
00:00:26.620 --> 00:00:32.120
且 checker / clock / reset / 接受端可信時，任何未授權交易不會 commit」。

7
00:00:32.120 --> 00:00:35.040
生活類比不取代產品威脅模型或評估認證。

8
00:00:35.375 --> 00:00:42.515
claim 需列資產與接受邊界、attacker能力、fault target/effect/timing/budget、

9
00:00:42.515 --> 00:00:46.555
trusted components、環境、design revision與排除項。

10
00:00:46.555 --> 00:00:52.555
每項證據標成 requirement、RTL review、simulation、formal、netlist、

11
00:00:52.555 --> 00:00:57.255
physical measurement 或 product test；不同等級不可互相代替。

12
00:00:57.255 --> 00:01:04.675
coverage 不只是一個百分比：列 target ×effect × time × lifecycle × reset/domain

13
00:01:04.675 --> 00:01:11.495
bins 的分母與空格；列 fault-free/authorizedcontrols、反例與重播 hash。

14
00:01:11.495 --> 00:01:16.095
將每個反例連到根因、修補提交、重新驗證結果。

15
00:01:16.095 --> 00:01:20.515
工具 unsupported 或無法觀察的項目列為unknown，不放到 covered。

16
00:01:20.833 --> 00:01:27.933
審查結論分「在範圍內未找到反例」「存在反例」「證據缺失」「假設無法驗證」。

17
00:01:27.933 --> 00:01:35.913
第一種不代表零風險。產品 release 要由責任人接受 residual risk，不能由模型摘要自動替代。

18
00:01:35.913 --> 00:01:45.153
包內放 claim ID、版本與來源、工具/命令、輸入與 seed、hash、分類規則、coverage matrix、

19
00:01:45.153 --> 00:01:49.453
失敗 trace、限制、未知項目、負責人與日期。

20
00:01:49.453 --> 00:01:56.173
讓審查者先從 claim 挑一條最可能推翻結論的路徑，再把反例與控制案例各重播一筆。

21
00:01:56.513 --> 00:02:03.073
以下為性質草案：先定義 harness 的transaction、reset 與 oracle，並確認取樣邊界，

22
00:02:03.073 --> 00:02:06.293
再接入設計；尚未編譯或證明。

23
00:02:06.293 --> 00:02:10.653
此片段不證明 CDC、timing、side-channel 或實體注入；

24
00:02:10.653 --> 00:02:13.573
需由各自工具與測量提供證據。

25
00:02:13.573 --> 00:02:20.173
審查者先挑一條最可能推翻claim的路徑，再找一筆反例和一筆控制案例重播。

26
00:02:20.173 --> 00:02:26.693
若版本、輸入、seed、工具命令或hash缺一項，重播就可能不是同一個實驗。

27
00:02:26.693 --> 00:02:33.253
coverage也要寫出分母：哪些target、effect、時間窗、lifecycle與reset分組曾測，

28
00:02:33.253 --> 00:02:42.393
哪些仍是空格。最後把證據分級，分清RTL檢視、模擬、formal、netlist、實體量測和產品測試。

29
00:02:42.393 --> 00:02:46.153
缺證據或無法觀察的項目維持unknown。

30
00:02:46.153 --> 00:02:50.573
只有責任人能接受殘餘風險，報表上的PASS不能代替這個決定。

31
00:02:50.930 --> 00:02:55.050
安全主張要限定資產、接受邊界和故障能力。

32
00:02:55.050 --> 00:02:58.790
信任元件、版本與排除項也要寫清楚。

33
00:02:58.790 --> 00:03:05.250
單一通過率、工具 PASS，或目前未找到反例，都不能抹去覆蓋空格與未驗假設。

34
00:03:05.250 --> 00:03:12.210
把每項 claim 連到可重播證據，列出 coverage分母、失敗 trace、修補與殘餘風險責任人。

35
00:03:12.210 --> 00:03:19.670
請另一位審查者用保存的版本、hash、命令、輸入和 seed，重播一筆反例及一筆控制案例。

36
00:03:19.670 --> 00:03:23.950
再檢查 coverage bins、限制與未知清單是否完整。

37
00:03:23.950 --> 00:03:30.450
缺少證據時，縮小結論範圍並記下缺口，由責任人決定是否接受殘餘風險。

38
00:03:30.450 --> 00:03:36.850
文件與模型證據只支持所列範圍，不能代替產品驗證、認證或風險決策。

39
00:03:36.850 --> 00:03:39.970
現在選一個尚未驗證的 CDC 假設。

40
00:03:39.970 --> 00:03:43.830
什麼最小證據可以支持它，由誰補齊？

41
00:03:43.830 --> 00:03:46.230
哪些缺口必須阻止 release？

42
00:03:46.230 --> 00:03:50.270
保留修訂紀錄，讓下一輪修補與重測能對照相同條件。