信任的架構：重新審視可證明安全作業系統 (PSOS)

在 1979 年，SRI International 的 Richard J. Feiertag 與 Peter G. Neumann 發布了《可證明安全作業系統 (PSOS) 的基礎》。雖然這篇論文是在雲端運算與無處不在的惡意軟體時代之前的數十年前撰寫的，但它概述了作業系統安全性的願景，至今仍具有驚人的相關性。PSOS 的核心不僅僅是在現有的核心 (kernel) 中添加安全性功能，而是使用形式化方法 (formal methods) 從底層開始構建系統，以確保安全性屬性在數學上是可證明的。

分層開發方法論 (HDM)

PSOS 是使用 SRI 分層開發方法論 (HDM) 設計的。與許多作業系統中常見的即興開發不同，HDM 依賴於正式陳述的需求與規範。系統被結構化為一系列分層組織的模組，其中每個模組的設計都使用一種稱為 SPECIAL 的語言進行正式規範。

這種方法允許進行兩步驟的形式化驗證過程：

規範驗證 (Specification Verification)：證明正式規範滿足所需的安全性需求。
實作驗證 (Implementation Verification)：證明實際的程式 (無論是在硬體、韌體或軟體中) 與這些規範是一致的。

核心機制：權限 (Capabilities)

PSOS 的定義性特徵是其對 capabilities 的統一使用。在 PSOS 中，一個 capability 是不可偽造的權杖 (token)，用於授予對某個物件的存取權限。如果一個程序 (process) 不持有該物件的 capability，它就絕對無法存取它。

Capability 的解剖結構

每個 capability 由兩個不可變的部分組成：

唯一識別碼 (UID)：一個由系統生成的 ID，用於唯一識別該物件。
存取權限 (Access Rights)：一個 Boolean 陣列，定義了允許哪些操作 (read, write, execute, delete)。

強制執行與安全性

為了防止程式偽造自己的 capability，PSOS 採用了 tagging 技術。在處理器與記憶體中，capability 會被標記一個使用者程式無法存取的 tag bit。這確保了 capability 不會被篡改或憑空產生；它只能由系統創建，或者透過 restrict_access 操作從現有的 capability 衍生而來，而該操作只能移除權限，絕不能增加權限（即單調性規則，the monotonicity rule）。

抽象與類型管理器 (Type Manager)

PSOS 將其功能組織成一個抽象層級結構，從 Level 0 (Capabilities) 到 Level 16 (User Request Interpretation)。這使得系統能夠在原始的物理資源 (如暫存器與中斷) 之上，構建複雜的虛擬資源 (如目錄與使用者程序)。

這裡的一個關鍵創新是 Type Manager。類型管理器是一個負責特定類型物件的程式。它將 capability 的 UID 映射到抽象物件的實際表示形式。由於 capability 機制非常簡單且位於系統的最底層，因此它可以統一應用於架構的所有層級，從而消除了為不同類型的系統物件提供特殊用途設施的需求。

PSOS 與核心 (Kernel) 方法的對比

Feiertag 與 Neumann 將 PSOS 與當時其他安全系統中常見的「核心 (kernel)」架構進行了對比。在傳統的核心方法中，一小段核心且必要的程式碼 (kernel) 被隔離以強制執行安全性政策。

然而，作者們認為，這往往會導致「受信任程序 (trusted processes)」——即核心之外、對安全性至關重要但未被標記為受信任的程式。這會使實際的 TCB (Trusted Computing Base) 膨脹，並使驗證變得複雜。

PSOS 採取了不同的路徑。PSOS 並非使用單一、僵化的核心來強制執行單一政策，而是提供了一個高度可擴展的框架。它允許創建多個子系統，每個子系統都充當特定任務的「核心」，從而使系統能夠同時支持多個、可能存在衝突的安全性政策。

現代反思：網際網路時代

雖然 PSOS 在 1979 年是一個理論基礎，但其哲學與現代安全挑戰產生了共鳴。在 Hacker News 的討論評論中，用戶指出，目前業界對防毒軟體層級、特徵碼與應用程式商店審核的依賴，是對一個根本性架構缺陷的反應式做法：缺乏基於 capability 的系統。

「我理解為什麼在 1979 年... capability OS 架構可能並不適用... 但在那之後，聽起來這似乎是唯一適合網際網路時代的架構，在這種情況下，你可以從任何地方下載並執行任何東西... 程式預設情況下根本沒有任何存取權限。」

今天，我們在虛擬化與容器化 (例如 Docker) 的崛起中看到了 PSOS 哲學的影子。透過將程式隔離在容器中，開發者實際上是在創建一個粗糙版本的、基於 capability 的隔離機制——即透過限制程序預設能「看到」與「觸碰」的內容，來降低第三方套件中惡意軟體的風險。

透過重新審視 PSOS，我們被提醒了：通往真正安全系統的路徑並非在於添加更多安全軟體，本身，而是在於設計一個安全性是系統本身固有的、可證明的屬性之架構。