ABSTRACTThis paper describes the design and implementation of a new operatingsystem authorization architecture to support trustworthy computing.Called logical attestation, this architecture provides a soundframework for reasoning about run time behavior of applications.Logical attestation is based on attributable, unforgeable statementsabout program properties, expressed in a logic. These statementsare suitable for mechanical processing, proof construction, and verification;they can serve as credentials, support authorization basedon expressive authorization policies, and enable remote principalsto trust software components without restricting the local user’schoice of binary implementations.We have implemented logical attestation in a new operating systemcalled the Nexus. The Nexus executes natively on x86 platformsequipped with secure coprocessors. It supports both nativeLinux applications and uses logical attestation to support newtrustworthy-computing applications. When deployed on a trustworthycloud-computing stack, logical attestation is efficient, achieveshigh-performance, and can run applications that provide qualitativeguarantees not possible with existing modes of attestation.
展开▼
