1979 年，SRI International 的 Richard J. Feiertag 与 Peter G. Neumann 在 AFIPS National Computer Conference 发表《The foundations of a provably secure operating system (PSOS)》。论文只有 9 页，目标却很硬：为“可证明安全”的操作系统设计一套基础。

有意思的地方在于，PSOS 不是在讲“内核里多加几道检查”。它问的是更底层的问题：系统对象怎么命名，权限怎么传递，模块边界怎么证明。如果这些东西一开始就是散的，后面补再多安全机制，也很难说清到底安全在哪里。

我更在意的也是这一点。PSOS 的关键价值，不是它后来有没有大规模部署，而是它把安全问题前移了：从补漏洞，前移到规格、分层抽象和不可伪造 capability 的系统设计层。

PSOS 先处理地基：需求、模块和连接关系都要能被说明

PSOS 基于 SRI 的 Hierarchical Development Methodology，简称 HDM。论文里说得很清楚，HDM 依赖三类正式材料：正式需求、每个模块的正式规格，以及模块之间连接关系的正式说明。

PSOS 的设计用 SPECIAL 这门 specification and assertion language 描述。系统被划分为约 20 个分层模块。第 0 层是 capability 机制，再往上支撑寄存器和存储、中断、时钟、I/O、页、段和窗口、抽象对象管理器、目录、用户进程、用户环境与名字空间等对象。

这套分层不是为了画架构图好看。它要做的是把安全证明的对象缩小、拆清楚。每个模块有规格，模块之间的连接也有说明，才有可能讨论“规格是否满足需求”。

这里也要把边界说准。论文没有宣称已经完成整个系统的代码级证明。更稳妥的说法是：HDM 让需求、规格和模块连接进入可证明的路径，并把程序与规格一致性证明作为目标。

以 1979 年的工具链条件看，这已经很激进。但它仍然不是今天很多人理解的“整套系统已经被完整机器验证”。

问题常见内核补丁式思路PSOS 的取向对今天的启发
安全从哪里开始代码里补检查从需求和模块规格开始安全评审要看规格，不只看功能清单
对象怎么访问各类资源各有规则所有对象经 capability 访问减少例外路径，方便审计
证明证明什么多数停在实现经验先证明规格满足需求，再追求程序一致性证明链条要分层，不要一句“已验证”带过
底层依赖默认软件内核处理可跨硬件、固件、软件实现硬件支持会改变安全边界

对做形式化验证的团队，这里有一个很实际的动作：评估一个“安全可证明”的系统时，不要只看论文或白皮书有没有证明章节。要追问三件事：需求是否形式化，模块边界是否稳定，实现和规格之间有没有一致性计划。

如果这三件事答不上来，采购可以延后，内部试点也应缩小范围。因为后续成本不会消失，只会转移到集成、审计和故障定位里。

capability 不是权限位：它同时负责命名和授权

PSOS 里的 capability 由两部分组成：唯一标识 uid 和访问权集合。创建之后，这两部分都不可修改。系统只为每个 uid 生成一个原始 capability，后续副本只能从原始 capability 直接或间接复制而来。

这和普通权限位不是一回事，也不是 ACL 换皮。

普通 ACL 更像是在对象旁边放一张名单，写着谁可以做什么。PSOS 的 capability 同时承担对象命名和访问控制。你持有它，才有办法指称这个对象；没有它，对象对你就不该存在为一个可访问目标。

论文强调 capability 不能伪造、不能篡改。它依赖处理器、主存和辅存中的硬件标签位，把 capability 和普通数据区分开。标签位对程序不可访问，因此程序不能把一段普通数据改造成 capability。

复制也被限制。副本通过 restrict_access 生成，新的访问权是原访问权和 mask 的交集。也就是说，只能收窄，不能扩大。

PSOS 还引入 store permissions，用来限制 capability 的传播。一个进程可以获得访问某对象的能力，但未必能把这份能力存进其他进程可读的目录、通信通道或存储段。

这点很关键。安全不只看“谁能访问”，还要看“能力能不能继续流出去”。很多权限模型的麻烦，正出在传播路径说不清。

对安全架构团队来说，PSOS 给出的不是一个可以照搬的实现方案，而是一组检查问题：

  • 对象命名和授权是不是分裂在两套机制里？
  • 权限复制能不能只缩小，不能放大？
  • 能力传播有没有单独限制，而不是默认谁拿到就能转交？
  • 底层系统是否能区分 capability 和普通数据？

现实约束也很硬。PSOS 的能力机制依赖硬件标签、能力存储和传播控制。把这套思路塞进既有通用操作系统，不会只是改几个权限接口。它会牵动处理器、内存、文件系统、进程模型和开发工具。

所以我不太买账把 PSOS 简单包装成现代安全口号的做法。它更像是在提醒我们：如果底层对象模型没有给安全留位置，上层策略会越来越像补苴罅漏。

今天重读 PSOS，最该看三条落点

PSOS 不是孤立出现的。更早的 capability 系统已经存在，比如 Cambridge CAP computer、Hydra、CAL-TSS 等项目。PSOS 的不同之处，是把 capability 放进 HDM 的分层开发框架里，让保护机制、抽象对象和形式化证明互相咬合。

这也是它对今天仍有价值的原因。不是因为它预言了某个现代产品，而是因为它把一个问题问得很早：安全到底是在系统建成后补出来，还是从对象模型和证明结构里长出来。

接下来观察类似思想是否真正落地，我会看三类变量，而不是看概念名字像不像。

观察点该看什么判断意义
硬件能力支持capability 是否由硬件或固件保护，普通程序能否伪造决定对象能力模型是不是只停在软件约定
形式化边界需求、模块规格、连接关系是否公开清楚决定“可证明”有没有落脚点
工程维护成本开发、调试、迁移工具是否跟得上决定研究原型能否进入长期系统

对操作系统研究者，PSOS 值得重读的是方法：不要只比较性能和接口，也要比较对象模型、权限流动和证明边界。

对工程团队，PSOS 的提醒更直接：如果要引入形式化验证、安全语言运行时、可信组件证明或硬件能力机器，不要把它当成单点工具采购。更现实的做法是先选一个边界清楚的组件试点，把需求、规格、接口和测试证据放在同一条链上。

如果团队现在连模块边界都频繁变动，就别急着把“可证明安全”写进目标。先把对象、权限和传播路径整理清楚。名不正，则言不顺；规格不清，证明也就站不住。

回到 1979 年那篇论文，PSOS 的超前不在于它已经给出了所有答案。它超前在把问题问到了地基上：安全不是最后贴上去的标签，而是系统一开始如何命名对象、限制能力、组织证明。