信任的架构：重新审视可证明安全操作系统 (PSOS)

在 1979 年，SRI International 的 Richard J. Feiertag 和 Peter G. Neumann 发表了《可证明安全操作系统的基础 (The foundations of a provably secure operating system (PSOS))》。虽然这篇文章写于云计算和无处不在的恶意软件现代时代之前的几十年，但它概述了一种对操作系统安全性的愿景，这种愿景在今天看来依然具有惊人的相关性。PSOS 的核心不仅仅是在现有内核中添加安全功能，而是使用形式化方法从头开始构建一个系统，以确保安全属性在数学上是可证明的。

分层开发方法论 (HDM)

PSOS 是使用 SRI 分层开发方法论 (HDM) 设计的。与许多操作系统中常见的即时开发不同，HDM 依赖于正式陈述的需求和规范。系统被结构化为一组分层组织的模块，其中每个模块的设计都使用一种称为 SPECIAL 的语言进行正式规范。

这种方法允许进行两步形式化验证过程：

规范验证：证明正式规范满足所需的安全需求。
实现验证：证明实际程序（无论是硬件、固件还是软件）与这些规范保持一致。

核心机制：能力 (Capabilities)

PSOS 的定义性特征是其对能力 (capabilities) 的统一使用。在 PSOS 中，能力是一种不可伪造的令牌，用于授予对对象的访问权限。如果一个进程不拥有某个对象的能力，它就无法访问该对象——绝无例外。

能力的解剖结构

每个能力由两个不可变的部分组成：

唯一标识符 (UID)：一个由系统生成的、用于唯一标识对象的 ID。
访问权限：一个布尔数组，定义了允许执行哪些操作（读、写、执行、删除）。

强制执行与安全性

为了防止程序伪造自己的能力，PSOS 采用了标记 (tagging) 技术。在处理器和内存中，能力被标记了一个用户程序无法访问的标记位 (tag bit)。这确保了能力无法被篡改或凭空创建；它只能由系统创建，或者通过 restrict_access 操作从现有能力派生而来，而该操作只能移除权限，绝不能增加权限（单调性规则)。

抽象与类型管理器

PSOS 将其功能组织成一个抽象层级，从 Level 0 (Capabilities) 到 Level 16 (User Request Interpretation)。这使得系统能够在原始物理资源（如寄存器和中断）之上构建复杂的虚拟资源（如目录和用户进程）。

这里的一个关键创新是类型管理器 (Type Manager)。类型管理器是一个负责特定类型对象的程序。它将能力的 UID 映射到抽象对象的实际表示。由于能力机制非常简单且位于系统的最低层，因此它可以统一应用于架构的所有层级，从而消除了为不同类型的系统对象提供专用设施的需求。

PSOS 与内核方法

Feiertag 和 Neumann 将 PSOS 与当时其他安全系统中常见的“内核”架构进行了对比。在传统的内核方法中，一小段核心代码（内核）被隔离以执行安全策略。

然而，作者认为，这往往会导致“受信任进程”——即内核之外的、对安全性仍然至关重要但未被标记为受信任的程序。这会使实际的 TCB (Trusted Computing Base) 膨胀，并使验证变得复杂。

PSOS 采取了不同的路线。PSOS 并不提供单一、僵化的内核来执行一种策略，而是提供了一个高度可扩展的框架。它允许创建多个子系统，每个子系统都充当特定任务的“内核”，从而使系统能够同时支持多个、潜在冲突的安全策略。

现代反思：互联网时代

虽然 PSOS 在 1979 年只是一个理论基础，但其哲学与现代安全挑战产生了共鸣。在 Hacker News 的讨论评论中，用户指出，当前行业对多层反病毒软件、特征码和应用商店审核的依赖，是对一个根本性架构缺陷的反应式做法：缺乏基于能力的系统。

"I understand why in 1979... capability OS architecture might have been irrelevant... But after that, it sounds like the only architecture suitable for the internet age, where you can download and run anything from anywhere... a program simply doesn'://t have access to anything by default."

今天，我们在虚拟化和容器化（例如 Docker）的兴起中看到了 PSOS 哲学的回响。通过将程序隔离在容器中，开发者实际上是在创建一种 PSOS 在几十年前提出的基于能力的隔离的粗略版本——通过默认限制进程可以“看到”和“触及”的内容，来减轻第三方包中恶意软件的风险。

通过重新审视 PSOS，我们被提醒：通往真正安全系统的路径不在于添加更多的安全软件，而是在于设计一种架构，使安全性成为系统本身固有的、可证明的属性。