HYDRA: hybrid design for remote attestation (using a formally verified microkernel)
HYDRA: hybrid design for remote attestation (using a formally verified microkernel)
复制标题
DOI：
10.1145/3098243.3098261
复制
发表时间：
2017-03
期刊：
影响因子：
--
通讯作者：
Karim M. El Defrawy;Norrathep Rattanavipanon;G. Tsudik
中科院分区：
文献类型：
--
作者：
Karim M. El Defrawy;Norrathep Rattanavipanon;G. Tsudik
远程证明（RA）允许一个可信实体（验证者）安全地测量远程不可信硬件平台（证明者）的内部状态。RA可用于在嵌入式和信息物理系统中建立静态或动态的信任根。它还可作为其他安全服务和原语（如软件更新和补丁、可验证删除以及内存重置）的构建模块。RA设计主要有三种类型：基于硬件的、基于软件的和混合的，每种都有其自身的优缺点。本文提出了第一种混合RA设计——称为HYDRA，它基于经过形式验证的软件组件构建，这些组件确保内存隔离和保护，并对内存和其他资源实施访问控制。HYDRA通过使用经过形式验证的seL4微内核获得这些特性。（到目前为止，这只有通过纯基于硬件的设计才能实现。）使用seL4对底层微处理器的硬件要求更低。此外，基于经过形式验证的软件组件构建增加了对HYDRA整体设计及其实现安全性的信心。我们在两个商用硬件平台上实例化HYDRA，并通过实验评估在这些平台上执行RA的性能和开销；我们表明，当使用基于Speck的加密校验和时，HYDRA能够在不到250毫秒内证明10MB的内存。
Remote Attestation (RA) allows a trusted entity (verifier) to securely measure internal state of a remote untrusted hardware platform (prover). RA can be used to establish a static or dynamic root of trust in embedded and cyber-physical systems. It can also be used as a building block for other security services and primitives, such as software updates and patches, verifiable deletion and memory resetting. There are three major types of RA designs: hardware-based, software-based, and hybrid, each with its own set of benefits and drawbacks. This paper presents the first hybrid RA design - called HYDRA - that builds upon formally verified software components that ensure memory isolation and protection, as well as enforce access control to memory and other resources. HYDRA obtains these properties by using the formally verified seL4 microkernel. (Until now, this was only attainable with purely hardware-based designs.) Using seL4 imposes fewer hardware requirements on the underlying microprocessor. Also, building upon a formally verified software component increases confidence in security of the overall design of HYDRA and its implementation. We instantiate HYDRA on two commodity hardware platforms and assess the performance and overhead of performing RA on such platforms via experimentation; we show that HYDRA can attest 10MB of memory in less than 250msec when using a Speck-based cryptographic checksum.