论文标题
忠实执行远程证明协议的基础架构
An Infrastructure for Faithful Execution of Remote Attestation Protocols
论文作者
论文摘要
远程证明是一种在远程计算系统中建立信任的新兴技术。科普兰是一种特定于领域的语言，用于指定分层证明协议，表征与证明相关的系统事件以及描述捆绑的证据。在这项工作中，我们正式定义并验证了用于执行科普兰协议的科普兰编译器和科普兰虚拟机。编译器将Copland转换为虚拟机上执行的说明。编译器和虚拟机在COQ证明助理中被实施为单一的功能程序，并在Copland事件和证据语义方面进行了验证。此外，我们将认证经理Monad作为管理Copland执行的环境，为管理Nonces提供支持，Copland协议对变量的约束成果以及评估证据结果。
Remote attestation is an emerging technology for establishing trust in a remote computing system. Copland is a domain-specific language for specifying layered attestation protocols, characterizing attestation-relevant system events, and describing evidence bundling. In this work we formally define and verify a Copland Compiler and Copland Virtual Machine for executing Copland protocols. The compiler translates Copland into instructions that are executed on the virtual machine. The compiler and virtual machine are implemented as monadic, functional programs in the Coq proof assistant and verified with respect to the Copland event and evidence semantics. In addition we introduce the Attestation Manager Monad as an environment for managing Copland term execution providing support for managing nonces, binding results of Copland protocols to variables, and appraising evidence results.
