形式化推理框架：组合系统安全的接口限制与递归编程语言

本文《组合系统安全性的形式化推理框架》发表在《理论计算机科学电子笔记》第265期（2010年），由Deepak Garg、Jason Franklin、Dilsun Kaynar和Anupam Datta四位作者来自美国卡内基梅隆大学。文章聚焦于解决可信计算领域的核心挑战——组合系统的安全性，尤其是在面对复杂组件交互时如何确保整体系统的安全性。 作者的核心观点是将可信系统的设计与接口安全相结合。他们提出一种新的视角，即把系统视为由公开接口连接的组件集合，攻击者被限制在接口级别，这意味着他们只能访问接口调用，而不能随意组合这些调用。这个框架是对现有系统正确性保证推理方法的扩展，考虑了一个未知具体策略的对手，强调了对系统动态行为的全面理解。 论文的核心内容包括开发了一个具有递归函数的表达性并发编程语言，用于精确建模接口和逻辑，从而支持组合推理原则的严谨形式化。文章通过一个理想化的文件系统示例，展示了如何通过跟踪语义来证明组合系统安全性的合理性。这种方法不仅关注静态的安全性分析，还考虑了动态环境下的对手行为。 文章指出，尽管在特定领域如信息流控制和密码协议中有了一些进展，但对于组合安全的一般性理论尚处于早期阶段。本文的贡献在于提供了一个更为通用的框架，能够处理不同类别对手的组合攻击，这对于理解和保护现代系统免受恶意利用至关重要。 关键词：组合系统安全、程序逻辑、时序逻辑。该研究工作旨在填补安全组合理论的空白，为未来设计和验证更加安全的系统提供了理论基础。