体系结构推理与信息安全：一种抽象验证方法

"使用体系结构推理信息安全的方法" 本文主要探讨了一种通过系统架构来推理和保障信息安全的方法。作者斯蒂芬·庄和罗恩·范德梅登指出，信息流的安全属性可以从系统的抽象架构描述中得到证明，这种方法关注的是系统的因果结构和组件的本地属性。他们提出了一种称为“概括不传递的不干扰政策”（non-interference policy），这种政策旨在限制和过滤不同通信域之间的信息传递，从而保护系统安全。 在信息安全领域，不干扰政策是一个关键概念，它确保在一个安全级别上的操作不会影响到其他安全级别的状态。在本文中，作者展示了一个自上而下的开发过程，即从高层次的架构规范开始，然后逐步细化，以此来证明信息安全属性。他们强调，这种体系结构的细化过程支持安全属性的验证，并且在特定的设置中，可以通过因果结构强制执行访问控制。 此外，作者还讨论了如何结合静态检查的访问控制设置和本地组件的验证来确保广义的不传递不干扰政策得到满足。这表明，通过对系统架构的深入理解和控制，可以实现更为精确的安全策略实施。 文章提到了几种关键的技术和概念，如信息流安全、认知逻辑、系统架构以及内在不干涉。这些技术都是为了构建和验证安全和隐私的正式模型。其中，认知逻辑可能用于表达和分析系统中的信息流和安全规则。系统架构则提供了一个框架，使得可以清晰地描述和分析组件间的交互和信息流动。 MILS（多独立安全级别）方法也被提及，这是一种依赖于架构来构建高保证系统的方法，但其具体实现还在不断发展。文章的更新版本包含了更多的研究成果，包括访问控制的实施和更详尽的示例，以进一步证明所提出的理论和方法的有效性。 这项研究得到了美国空军科学研究办公室、澳大利亚研究委员会和国家科学基金会的支持，体现了这些机构对于信息安全领域基础研究的重视。本文为理解和实施基于体系结构的信息安全保障提供了一种理论和实践相结合的视角，对于信息安全和系统架构的设计者与研究人员具有重要的参考价值。