一种用于忠实执行远程证明协议的基础设施
密码学与安全
2020-12-22 v1 计算机科学中的逻辑
编程语言
摘要
远程证明是一种用于建立对远程计算系统信任的新兴技术。Copland 是一种领域特定语言，用于指定分层证明协议、刻画与证明相关的系统事件以及描述证据捆绑。在这项工作中，我们形式化定义并验证了用于执行 Copland 协议的 Copland 编译器和 Copland 虚拟机。该编译器将 Copland 翻译为在虚拟机上执行的指令。编译器和虚拟机作为单子化函数式程序在 Coq 证明助手中实现，并依据 Copland 事件与证据语义进行了验证。此外，我们引入了证明管理器单子（Attestation Manager Monad）作为管理 Copland 项执行的环境，提供对随机数管理、将 Copland 协议结果绑定到变量以及评估证据结果的支持。
引用
@article{arxiv.2012.10511,
title = {An Infrastructure for Faithful Execution of Remote Attestation Protocols},
author = {Adam Petz and Perry Alexander},
journal= {arXiv preprint arXiv:2012.10511},
year = {2020}
}