Verifying Hardware Security Modules with Information-Preserving Refinement-猫眼课题宝

DOI：

发表时间：

2022

期刊：

影响因子：

通讯作者：

中科院分区：

其他

文献类型：

作者：

Anish Athalye;M. Kaashoek;Nickolai Zeldovich

Knox 是一个新框架，使开发人员能够通过形式验证构建高度可靠的硬件安全模块 (HSM)。目标是排除所有硬件错误、软件错误和定时侧通道。诺克斯的方法是将实现的线路级行为与以方法调用和返回值表示的功能规范相关联，并使用称为信息保留细化（IPR）的新定义。该定义捕获了 HSM 实现其功能规范的概念，并且它不会通过其线路级行为泄漏任何其他信息。 Knox 框架支持编写规范、导入用 Verilog 和 C 代码编写的 HSM 实现，以及使用轻量级注释和交互式证明的组合来证明 IPR。为了评估 IPR 定义和 Knox 框架，我们验证了三个简单的 HSM，包括符合 RFC 6238 的 TOTP 令牌。 TOTP 令牌是用 2950 行 Verilog 和 360 行 C 和汇编语言编写的。它的行为被描述在一个简洁的规范中：除了 TOTP 算法的定义之外，规范只有 10 行代码。在所有三个案例研究中，验证涵盖了整个硬件和软件堆栈，并排除了硬件/软件错误和定时侧通道。

Knox is a new framework that enables developers to build hardware security modules (HSMs) with high assurance through formal veriﬁcation. The goal is to rule out all hardware bugs, software bugs, and timing side channels. Knox’s approach is to relate an implementation’s wire-level behavior to a functional speciﬁcation stated in terms of method calls and return values with a new deﬁnition called information-preserving reﬁnement (IPR) . This deﬁnition captures the notion that the HSM implements its functional speciﬁcation, and that it leaks no additional information through its wire-level behavior. The Knox framework provides support for writing speciﬁcations, importing HSM implementations written in Verilog and C code, and proving IPR using a combination of lightweight annotations and interactive proofs. To evaluate the IPR deﬁnition and the Knox framework, we veriﬁed three simple HSMs, including an RFC 6238-compliant TOTP token. The TOTP token is written in 2950 lines of Verilog and 360 lines of C and assembly. Its behavior is captured in a succinct speciﬁcation: aside from the deﬁnition of the TOTP algorithm, the spec is only 10 lines of code. In all three case studies, veriﬁcation covers entire hardware and software stacks and rules out hardware/software bugs and timing side channels.

Verifying Hardware Security Modules with Information-Preserving Refinement

文献摘要

被引文献

相似文献