PSOS：1979年形式化验证操作系统的能力模型设计与现代启示

在操作系统安全领域，形式化验证从学术研究走向工程实践经历了漫长的演进。1979 年，SRI International 计算机科学实验室的 Richard J. Feiertag 与 Peter G. Neumann 发表的 PSOS（Provably Secure Operating System）设计，首次系统性地将分层开发方法论与能力模型结合，构建了一个可被证明安全的操作系统架构。这一工作不仅奠定了后续四十年安全操作系统研究的理论基础，更为今天的微内核设计与形式化验证实践提供了关键的设计范式。

分层验证架构：从抽象到实现的形式化映射

PSOS 的核心创新在于采用 SRI 分层开发方法论（Hierarchical Development Methodology, HDM）指导整个系统的设计与验证。HDM 要求系统按照抽象层次逐层细化，每一层都通过形式化规范定义其行为，并证明下层实现满足上层规范。这种分层结构使得安全属性的验证可以在适当的抽象级别进行，避免了在实现细节中直接处理复杂的安全证明。

在 PSOS 的架构中，系统被组织为多个层次化的抽象机，每一层都建立在下层提供的服务之上。上层不需要了解下层的具体实现，只需要依赖下层暴露的接口规范。这种设计带来的直接好处是安全属性的可组合性：如果每一层都被证明满足其安全规范，那么整个系统的安全属性可以通过层次间的组合推理得到保证。对于现代安全操作系统设计者而言，这一原则仍然适用 —— 将系统分解为可验证的模块，并在模块边界处明确定义安全契约，是控制形式化验证复杂度的关键策略。

能力模型：细粒度访问控制的基础机制

PSOS 选择能力（capability）作为其核心安全机制，这一设计决策体现了对最小权限原则的深刻理解。在 PSOS 的能力模型中，每个对象（文件、进程、设备等）的访问权限都封装在一个不可伪造的能力令牌中。能力令牌是带有标签的、系统级保护的数据结构，用户态代码无法伪造或篡改。

能力的统一性是 PSOS 设计的显著特征。无论是文件、进程还是硬件资源，都通过相同的能力机制进行访问控制。这种统一性简化了安全策略的表达和验证 —— 安全模型只需要处理一种访问控制原语，而不需要为不同类型的资源维护多套机制。能力携带的访问权限是细粒度的，可以精确到读、写、执行等具体操作，这使得最小权限原则能够在实践中被严格执行。

更重要的是，PSOS 的能力模型支持能力的传递与委托，同时保持不可伪造性。当一个进程需要将某个资源的访问权限授予另一个进程时，它可以将能力复制给目标进程，但接收方无法提升权限或伪造新的能力。这种设计为现代操作系统中的权限委托模式（如 Android 的 Binder 机制、Fuchsia 的通道能力）提供了理论原型。

形式化方法在操作系统设计中的工程化挑战

PSOS 项目始于 1973 年，持续到 1980 年代初期，期间面临的工程化挑战至今仍有参考价值。形式化验证的计算成本是当时的主要瓶颈 —— 对完整操作系统进行定理证明所需的计算资源远超当时硬件的能力。PSOS 的解决方案是采用分层验证策略，将验证工作分散到各个抽象层，并在层间使用更轻量的证明技术。

另一个关键挑战是形式化规范与现实实现之间的鸿沟。PSOS 通过 HDM 的逐步细化过程来缓解这一问题：高层规范使用抽象数学语言表达安全属性，中层规范定义系统接口的行为契约，低层实现则对应具体的代码。每一层细化都需要证明正确性，这种 "验证伴随开发" 的模式比事后验证更符合工程实践。

对于今天的系统开发者，PSOS 的经验表明形式化验证并非全有或全无的选择。可以从关键组件开始，逐步扩展验证范围；可以混合使用不同强度的验证技术（如模型检验、类型系统、定理证明）；更重要的是，架构设计阶段就需要考虑可验证性，而非事后修补。

从 PSOS 到现代系统：能力模型的复兴

PSOS 的能力模型设计在沉寂数十年后，随着微内核架构的复兴而重新获得关注。seL4 微内核作为首个经过完整形式化验证的操作系统内核，其能力模型直接继承了 PSOS 的设计思想。seL4 使用能力控制所有内核对象的访问，能力的不可伪造性由内核保证，能力的传递通过系统调用实现。

Google 的 Fuchsia 操作系统同样采用能力模型作为其安全架构的基础。在 Fuchsia 中，命名空间、文件句柄、服务连接等都通过能力表示，进程间的通信通过能力传递实现。这种设计与 PSOS 的愿景高度一致 —— 通过统一的能力机制实现细粒度的访问控制和安全的资源管理。

现代 Web 平台的 Capability-based 安全模型（如 WebAssembly 的 capability-based 内存隔离、W3C 的 FedCM 提案）也可以追溯到 PSOS 的思想源头。这些现代实现受益于四十年来编程语言和形式化方法领域的进步，使得 PSOS 时代的理论构想能够在实际系统中落地。

对当前实践的启示

PSOS 项目留给当代系统设计者的重要启示包括：

架构先于实现：安全属性必须在架构设计阶段就纳入考量。PSOS 的分层架构使得安全验证成为可能，而事后添加安全机制往往只能获得有限的安全保证。

统一机制优于特殊处理：PSOS 的能力模型证明了统一的安全原语可以简化系统设计和验证。现代系统中过多的特殊权限机制（root、sudo、 capabilities、SELinux 策略等）往往导致安全策略的复杂性和不一致性。

形式化方法需要工程化集成：PSOS 的经验表明形式化验证需要与开发流程深度集成，而非作为独立的质量保证活动。HDM 的分层细化过程本质上是一种将验证嵌入开发的方法论。

可验证性是设计约束：设计决策应当考虑其对可验证性的影响。某些设计模式（如全局可变状态、隐式控制流）会显著增加形式化验证的难度，在关键组件中应当避免。

结语

PSOS 作为操作系统安全研究历史上的里程碑，其价值不仅在于提出了可被证明安全的系统架构，更在于展示了形式化方法在复杂系统工程中的应用路径。从 1979 年的理论构想到今天 seL4、Fuchsia 等系统的工程实践，能力模型与分层验证的思想经历了从学术原型到生产系统的完整演进。对于正在构建下一代安全系统的开发者而言，回顾 PSOS 的设计决策与经验教训，有助于在形式化验证的严谨性与工程实践的实用性之间找到平衡点。

参考来源

• Feiertag, R.J. & Neumann, P.G. (1979). The foundations of a provably secure operating system (PSOS). SRI International Computer Science Laboratory.
• SRI International Computer Science Laboratory. PSOS Project Documentation. https://www.csl.sri.com/papers/psos/

systems