一种经过验证的信息流体系结构
A Verified Information-Flow Architecture
摘要：
SAFE是高度安全的计算机系统的全新设计，具有用于跟踪和限制信息流的普遍机制。在最低级别，SAFE硬件支持细粒度的可编程标记，在执行指令时具有有效和灵活的标记传播和组合。操作系统将这些通用设施虚拟化，以呈现一个信息流抽象机，该信息流抽象机允许用户程序使用丰富的机密性策略来标记敏感数据。我们提出了一个正式的，机器检查模型的关键硬件和软件机制，用于动态控制信息流的安全和端到端的证明，该模型的非干扰。我们使用一个改进的证明方法来传播的抽象机器的不干扰属性到具体的机器级别。我们使用一个中间层的细化链，因素的信息流控制策略的细节，并设计一个代码生成器编译成低级别的监控代码的信息流策略。最后，我们使用一个专用的霍尔逻辑，从低级别的机器指令抽象成一组可重用的验证结构化代码生成器验证此生成器的正确性。
英文摘要：
SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to dynamically control information flow in SAFE and an end-to-end proof of noninterference for this model. We use a refinement proof methodology to propagate the noninterference property of the abstract machine down to the concrete machine level. We use an intermediate layer in the refinement chain that factors out the details of the information-flow control policy and devise a code generator for compiling such information-flow policies into low-level monitor code. Finally, we verify the correctness of this generator using a dedicated Hoare logic that abstracts from low-level machine instructions into a reusable set of verified structured code generators.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
