A verified information-flow architecture
A verified information-flow architecture
复制标题
经过验证的信息流架构
DOI：
10.1145/2535838.2535839
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
A. Tolmach
中科院分区：
文献类型：
--
作者：
Arthur Azevedo de Amorim;Nathan Collins;A. DeHon;Delphine Demange;Cătălin Hriţcu;David Pichardie;B. Pierce;R. Pollack;A. Tolmach
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 control information flow in SAFE and an end-to-end proof of noninterference for this model.