QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment
QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment
复制标题
QIF-Verilog：用于硅前安全评估的基于定量信息流的硬件描述语言
DOI：
10.1109/hst.2019.8740840
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Yier Jin
中科院分区：
文献类型：
--
作者：
Xiaolong Guo;R. Dutta;Jiaji He;M. Tehranipoor;Yier Jin
硬件漏洞通常是由于设计错误所致，因为设计师在设计阶段没有足够的考虑安全漏洞。结果，已经开发了各种安全解决方案来保护IC，其中基于语言的硬件安全验证是有前途的解决方案。验证过程将在编译设计的HDL时执行。但是，类似于其他正式验证方法，基于语言的方法也遇到了可扩展性问题。此外，现有的解决方案要么导致硬件开销，要么不是为脆弱或恶意逻辑检测而设计的。为了减轻这些挑战，我们提出了一个新的基于语言的框架QIF-Verilog，以评估寄存器传输级别（RTL）上硬件系统的可信度。该框架介绍了量化的信息流（QIF）模型，并扩展了Verilog类型系统，以提供更高的表达性，以呈现安全规则； QIF能够检查硬件设计师给出的安全规则。秘密用新类型标记，然后分解为数据流，将应用QIF模型。为了展示我们的方法，我们设计了QIF-Verilog的编译器，并对来自Trust-Hub和OpenCore的基准测试进行脆弱性分析。我们表明，可以自动检测到从电路输出中泄漏信息的特洛伊木马或设计故障，并且我们的方法正确评估了设计的安全性。
Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issue. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically, and that our method evaluates the security of the design correctly.