Logical attestation: an authorization architecture for trustworthy computing
Logical attestation: an authorization architecture for trustworthy computing
复制标题
逻辑证明：可信计算的授权架构
DOI：
10.1145/2043556.2043580
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
F. Schneider
中科院分区：
文献类型：
--
作者：
E. G. Sirer;W. D. Bruijn;Patrick Reynolds;Alan Shieh;Kevin Walsh;Dan Williams;F. Schneider
本文描述了一种新的操作系统授权架构的设计与实现，该架构用于支持可信计算。这种架构被称为逻辑证明，它为推理应用程序的运行时行为提供了一个合理的框架。逻辑证明基于用逻辑表达的关于程序属性的可归因且不可伪造的陈述。这些陈述适用于机械处理、证明构建和验证；它们可作为凭证，支持基于表达性授权策略的授权，并使远程主体能够信任软件组件，同时不限制本地用户对二进制实现的选择。我们已在一个名为Nexus的新操作系统中实现了逻辑证明。Nexus在配备安全协处理器的x86平台上原生执行。它既支持原生Linux应用程序，又使用逻辑证明来支持新的可信计算应用程序。当部署在可信云计算栈上时，逻辑证明是高效的，可实现高性能，并且能够运行提供现有证明模式无法实现的定性保证的应用程序。
This paper describes the design and implementation of a new operating system authorization architecture to support trustworthy computing. Called logical attestation, this architecture provides a sound framework for reasoning about run time behavior of applications. Logical attestation is based on attributable, unforgeable statements about program properties, expressed in a logic. These statements are suitable for mechanical processing, proof construction, and verification; they can serve as credentials, support authorization based on expressive authorization policies, and enable remote principals to trust software components without restricting the local user's choice of binary implementations. We have implemented logical attestation in a new operating system called the Nexus. The Nexus executes natively on x86 platforms equipped with secure coprocessors. It supports both native Linux applications and uses logical attestation to support new trustworthy-computing applications. When deployed on a trustworthy cloud-computing stack, logical attestation is efficient, achieves high-performance, and can run applications that provide qualitative guarantees not possible with existing modes of attestation.