PSOS 分层能力安全设计：1979年可证明安全操作系统的方法论遗产

引言：当安全成为可证明的命题

1979 年，斯坦福研究院（SRI）的 Peter Neumann 与 Richard Feiertag 发表了一篇题为《The foundations of a provably secure operating system (PSOS)》的论文。在操作系统安全仍主要依赖 "测试 - 修复" 循环的年代，PSOS 提出了一个激进的目标：通过形式化方法，在数学层面证明操作系统的安全属性。

这不是一个单纯的学术构想。PSOS 的设计者意识到，传统操作系统将安全视为事后补丁的做法存在根本性缺陷 —— 漏洞的发现往往发生在系统部署之后，而修复成本随时间呈指数级增长。因此，PSOS 尝试将安全属性内建于系统设计的每一个层级，并通过严格的层次化开发方法论（Hierarchical Development Methodology, HDM）确保这些属性在实现过程中不被破坏。

16 层架构：从硬件到用户空间的渐进抽象

PSOS 的核心架构由 16 个抽象层组成（编号 0-15），每一层都建立在前一层提供的原语之上，形成严格的功能依赖关系。这种设计并非简单的模块化拆分，而是基于 "安全属性逐层累积" 的哲学。

最底层（Layer 0）是整个系统的基石：能力（Capability）。这一层直接操作硬件资源，提供最基本的对象访问原语。向上逐层扩展，Layer 1 处理寄存器和存储，Layer 2 管理中断，Layer 3 实现时钟，直到 Layer 15 和 16 提供用户环境、命名空间和请求解释。

这种分层架构的关键在于信息隐藏与权限最小化。每一层只暴露必要的接口给上一层，而安全敏感的操作被封装在底层。例如，进程间通信（IPC）机制在 Layer 6 实现，它无法直接操作 Layer 0 的能力令牌，只能通过 Layer 5 提供的原语发起请求。这种设计使得安全策略的执行点高度集中，便于形式化验证。

能力式访问控制：不可伪造的安全令牌

PSOS 安全模型的核心是其能力（Capability）机制。与传统 Unix 的权限模型（基于用户 ID 和访问控制列表）不同，PSOS 采用纯能力式安全：访问权限不是询问 "你是谁"，而是验证 "你持有什么"。

在 PSOS 中，能力是一个不可伪造、不可更改的数据结构，包含三个关键要素：

1. 唯一对象标识符：指向系统中的一个具体资源（文件、内存段、设备等）
2. 访问权限集合：定义持有者对该资源可执行的操作（读、写、执行等）
3. 完整性保护：能力本身由操作系统内核保管，用户进程只能通过句柄（handle）间接引用

能力的关键特性在于可传递性与可降级。一个进程可以将能力传递给另一个进程，但只能传递相同或更严格的权限子集。例如，持有某文件读写能力的进程可以生成一个仅包含读权限的新能力给子进程，但无法提升自己或他人的权限。这种设计天然支持最小权限原则（Principle of Least Privilege），避免了传统模型中 "获得 root 即获得一切" 的困境。

形式化验证：SPECIAL 语言与 HDM 方法

PSOS 的野心不仅在于设计一个安全的系统，更在于证明它是安全的。为此，SRI 团队开发了 SPECIAL（SPECIfication and Assertion Language）规格说明语言，以及配套的分层开发方法论 HDM。

SPECIAL 允许设计者在每个抽象层定义不变式（invariant）和安全属性，然后使用形式化技术验证：

• 层内实现是否满足规格说明
• 高层抽象是否正确使用低层原语
• 安全属性在层间转换时是否保持

HDM 将开发过程分为设计、数据表示和实现三个阶段，每个阶段都有对应的验证目标。这种 "验证驱动" 的开发模式在当时极为超前 —— 直到 2009 年 seL4 微内核的形式化验证完成，学术界才重新大规模关注操作系统形式化验证。

现代回响：从 PSOS 到 Fuchsia 与 seL4

尽管 PSOS 本身并未成为商业产品，其设计思想深刻影响了后来的安全操作系统研究。最直接的继承者是能力式安全模型的持续演进：

• EROS/KeyKOS：延续纯能力式架构，强调持久化能力
• seL4：2009 年完成形式化验证的微内核，采用类似的分层验证方法
• Fuchsia：Google 开发的操作系统，使用能力式句柄管理所有资源访问
• Genode：基于能力隔离的组件化操作系统框架
• FreeBSD Capsicum：将能力式安全模型引入传统 Unix 系统

这些现代系统的共同点是：它们都采用了某种形式的 "令牌 + 权限" 模型，而非传统的 "身份 + ACL" 模型。在微服务架构和零信任网络日益普及的今天，PSOS 的 "持有能力即拥有权限" 思想显得尤为前瞻 —— 它本质上是一种去中心化的访问控制，不依赖全局可信的授权服务器。

局限与反思：形式化验证的现实约束

然而，PSOS 的方法论也存在明显的时代局限。16 层严格分层架构虽然利于验证，却与现代软件工程的敏捷实践存在张力：

跨层调用的性能开销：每一层抽象都带来额外的上下文切换和参数检查。在 1979 年的硬件环境下，这种开销或许可接受，但在追求微秒级延迟的现代系统中，严格分层可能成为瓶颈。

形式化验证的成本：完整验证一个复杂操作系统需要巨大的时间和人力投入。seL4 的验证耗时约 5 人年，而现代 Linux 内核的复杂度远超 PSOS 时代的想象。这导致形式化验证目前主要适用于安全关键的小型组件（如微内核、加密模块），而非完整操作系统。

安全边界的漂移：PSOS 假设安全威胁主要来自进程间的非法访问，但现代攻击面已扩展到侧信道、供应链、硬件漏洞等层面。形式化验证可以证明 "设计满足规格"，但无法保证 "规格覆盖所有威胁"。

可落地的设计启示

尽管完整复刻 PSOS 不切实际，其设计思想仍可为现代系统安全提供具体指导：

1. 能力式句柄的显式传递 在微服务架构中，将访问权限封装为可传递的令牌（如 JWT、macaroon），而非依赖隐式的会话状态。服务 A 调用服务 B 时，应传递一个仅包含必要权限的受限令牌，而非 A 的完整身份凭证。

2. 分层安全策略的集中执行点 识别系统中的 "安全敏感原语"（如密钥访问、特权操作），将它们集中到最底层，上层只能通过受限接口调用。这种设计使得安全审计和漏洞修复更加聚焦。

3. 权限的显式降级 在进程创建、容器启动、服务调用时，显式声明所需的权限子集，而非继承父进程的全部权限。现代容器安全工具（如 gVisor、seccomp）已部分实现这一思想。

结语

PSOS 代表了一种理想主义的安全观：安全不应是事后补丁，而应是系统设计的内生属性。40 多年后，虽然我们仍未实现 "可证明安全的通用操作系统"，但 PSOS 的能力模型和分层验证方法仍在影响 seL4、Fuchsia 等现代系统的设计。

在供应链攻击、勒索软件泛滥的今天，重新审视 PSOS 的遗产具有特殊意义。形式化验证或许无法解决所有安全问题，但 "将安全内建于设计" 的理念 —— 通过不可伪造的能力令牌、严格的分层抽象、显式的权限传递 —— 为构建真正可信的计算环境提供了历久弥新的方法论基础。

参考来源

1. Neumann, P. G., & Feiertag, R. J. (1979). The foundations of a provably secure operating system (PSOS). Proceedings of the National Computer Conference, 48:329-334.
2. Morrow, S. (2019). Provably Secure Operating Systems. Infosec Institute.
3. Capability-based security. Wikipedia.

systems