面向远程证明的形式化验证软硬件协同设计
密码学与安全
2019-05-28 v4
摘要
在这项工作中，我们朝着远程证明（RA）的形式化验证迈出了第一步，通过设计并验证一种称为 VRASED（用于简单嵌入式设备的可验证远程证明）的架构。VRASED 实例化了一种面向低端嵌入式系统（例如简单的 IoT 设备）的混合（硬件/软件）RA 协同设计。VRASED 提供了与基于硬件的方法相当的安全级别，同时依靠软件来最小化额外的硬件成本。由于安全属性必须由硬件和软件共同保证，验证是一项具有挑战性的任务，此前在 RA 领域从未尝试过。我们相信 VRASED 是首个形式化验证的 RA 方案。据我们所知，它也是任何安全服务的硬件/软件实现的首个形式化验证。为了证明 VRASED 的实用性和低开销，我们在一个商用平台（TI MSP430）上实例化并评估了它。VRASED 的公开可用实现已部署在 Basys3 FPGA 上。
引用
@article{arxiv.1811.00175,
title = {Formally Verified Hardware/Software Co-Design for Remote Attestation},
author = {Ivan De Oliveira Nunes and Karim Eldefrawy and Norrathep Rattanavipanon and Michael Steiner and Gene Tsudik},
journal= {arXiv preprint arXiv:1811.00175},
year = {2019}
}