證據優先文件 是做什麼的?
文件不是關於系統的故事。它是聲明分類帳:每個實質陳述都必須可追溯至機制與證據,且其限制條件必須與聲明一同陳述。
自信的句子很容易寫。真正的任務是讓讀者能夠分辨哪些是已被證明的、哪些是已被測試的、哪些僅經審查,以及哪些仍是懸而未決的。
核心規則
每個實質聲明都包含四項要素:
- 機制 — 系統中應使該聲明成立的部分。
- 證據 — 證明產物:證明、模型、測試、分析報告、追蹤、基準測試或審查記錄。
- 範圍 — 聲明適用的區域以及信任邊界之外的範圍。
- 狀態 — 證據所能支持的最強誠實標籤。
若缺少其中一項,則該聲明尚未準備就緒。將其改寫為設計意圖、計畫或開放性問題 — 不要將其偽裝成結果。
聲明分類帳
在文件中或連結的證據文件中維護一個表格:
| ID | 聲明 | 機制 | 證據 | 範圍 / TCB | 狀態 | 限制 | 最後驗證日期 |
|---|---|---|---|---|---|---|---|
| C-01 | 只有角色 X 可以寫入資料表 T | 權限檢查 + 資料庫政策 | 負向測試 T-04..T-11 | PostgreSQL 14–17;角色 Y、非角色 session | 已測試 | 超級使用者與 DBA 不在威脅模型內 | 2026-11-02 |
規則:
- 一行一個聲明,而非一行一個文件。
- 聲明必須是可證偽的。「系統是安全的」不是一個聲明;「角色 Y 無法通過任何受支援的端點寫入 T」才是。
- 連結產物,而不僅僅是工具名稱。「SARIF」是一種格式;報告路徑與已審查的規則集才是證據。
- 當產物重新執行時,更新「最後驗證日期」;過時的證據是發現項目,而非形式上的手續。
- 保留負向結果。「我們嘗試破壞它,但因 X 而失敗」是證據;隱藏它會產生虛假的安全感。
狀態階層
使用證據所能支持的最強標籤,切勿使用更強的標籤:
| 狀態 | 意義 |
|---|---|
已證明 | 對所陳述屬性的機器檢查證明,並宣告假設與 TCB |
模型已檢查 | 對模型的窮盡或有邊界探索;說明邊界與模型到程式碼的差距 |
已測試 | 執行的測試嘗試違反該屬性,並記錄環境與結果 |
靜態精煉 | 靜態分析或精煉檢查;說明工具、規則與未解決的發現項目 |
已審查 | 僅經人工審查;無可執行或正式的證據 |
開放 | 聲明存在但證據不存在;這是風險,而非結果 |
較低的狀態並非失敗。膨脹的狀態才是。
請勿在沒有相鄰狀態與範圍的情況下使用「已驗證」、「已證明」、「正確」、「安全」、「安全」、「完整」、「有保證」、「已認證」或「合規」等詞。如果該詞在沒有證據的情況下依然成立,就刪除該詞。
證據強度
偏好能因正確原因而失敗的證據:
- 在明確假設下對所陳述屬性的形式證明。
- 在陳述邊界內的窮盡模型檢查。
- 基於屬性或模糊測試,並記錄語料庫與預言機。
- 當機制被移除時會失敗的針對性負向測試。
- 使用已審查規則集與分類發現項目的靜態分析。
- 指定審查者與檢查清單的程式碼審查。
- 斷言或軼事。
階層並非絕對:一個針對性測試可能比誤用的證明更強。將證據與聲明匹配。一個不精煉程式碼的模型證明,並不能證明程式碼。一個因平台先行拒絕而通過的測試,並不能證明你的防護措施。
範圍與信任邊界
在聲明旁邊說明邊界,而非在遙遠的附錄中:
- 涵蓋的版本與平台。
- 排除的特權角色:超級使用者、DBA、部署管理員、密碼管理員、建置系統、操作員。
- 假設:密碼學基元、時鐘、網路、儲存、租戶隔離、配置。
- 哪些是符號建模的,哪些是真實執行的。
- 哪些超出範圍及原因。
一個未經限定的聲明是關於所有事物的聲明,這幾乎總是錯的。「在 PostgreSQL 14–17 上,使用文件化的配置,對角色 Y 是安全的;DBA 不在模型中」是真實且有幫助的。
工作流程
- 清點聲明。 閱讀文字,標記每個斷言屬性、結果、保證或合規狀態的句子。
- 分類每個聲明。 它是設計意圖、需求、實做事實、測試結果、形式結果,還是發行聲明?
- 分配 ID 與狀態。 添加機制、證據、範圍、限制與「最後驗證日期」。
- 根據產物測試該聲明。 打開報告、重新執行命令,或要求缺少的產物。不要僅接受檔案名稱作為證據。
- 改寫不支持的聲明。 將其轉換為「設計意圖」、「計畫中」、「尚未驗證」或開放性問題。保留其抱負;移除虛假的確定性。
- 檢查負向部分。 對於每個安全或正確性聲明,說明嘗試違反它的測試或分析。如果沒有,將該聲明標記為
開放。 - 審查語言。 移除禁用詞、模糊量詞與未經限定的絕對詞。請參閱
references/banned-words.md。 - 凍結證據。 記錄命令、提交、環境、日期與產物路徑,以便審查者可以重現結果。
- 設為發行門檻。 發行說明只能聲明分類帳所支持的內容。明確列出殘餘風險與開放聲明。
審查檢查清單
- 每個實質聲明都有 ID、機制、證據、範圍、狀態與限制。
- 每個
已測試聲明都命名了一個能在機制被移除時失敗的測試。 - 每個
模型已檢查聲明都說明了邊界與模型到程式碼的差距。 - 每個
已證明聲明都說明了假設與 TCB。 - 負向結果與已知失敗皆存在,而非被過濾掉。
- 日期與版本是最新的;過時的證據被標記為過時。
- 命名了特權角色與超出範圍的路徑。
- 在沒有相鄰證據與範圍的情況下,不出現任何禁用詞。
- README、架構文件、API 合約與發行說明之間互相不矛盾。
- 讀者可以僅從文件中重現證據。
反模式
- 抱負性現在式。 「系統強制執行...」但這只是個計畫。
- 以檔案名稱為證據。 「請參閱 report.pdf」但沒有結果、範圍或日期。
- 以工具名稱為證明。 「已通過靜態分析驗證」但沒有規則、發現項目與分類處理。
- 範圍洗白。 一個窄範圍的測試結果被呈現為產品範圍的保證。
- 綠色測試套件絕對主義。 「所有測試通過」但未說明哪些測試、在哪些平台上、以及它們試圖違反什麼。
- 合規 cosplay。 標準名稱被用作證書;對照表並非稽核。
- 隱藏的限制。 免責聲明存在但遠離聲明位置。
- 過時的確定性。 來自舊提交的結果被呈現為最新。
- 無負向證據。 只記錄成功;失敗與拒絕消失。
輸出格式
當被要求撰寫或審查技術文件時,請產出:
- 一個簡短的聲明摘要,按狀態統計數量。
- 聲明分類帳(內聯或連結)。
- 開放聲明與殘餘風險,明確與結果分離。
- 範圍與假設,緊鄰其所約束的聲明。
- 證據索引,包含路徑、命令、日期與版本。
使用 references/evidence-template.md 作為分類帳與發行說明的格式。在發佈前使用 references/banned-words.md。如果儲存庫包含標準對照表,它位於 references/standards-map.md;此技能本身不依賴任何標準。
根據文件規模調整輸出。簡短的發行說明需要緊湊的聲明表格與簡短的殘餘風險章節,而非完整的稽核包。認證證據文件需要完整的分類帳、證據索引與範圍。不要混淆詳盡性與長度;每一行都必須承載讀者所需的資訊。