| Title | QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | Guo, Xiaolong, Dutta, Raj Gautam, He, Jiaji, Tehranipoor, Mark M., Jin, Yier |
| Conference Name | 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST) |
| Date Published | may |
| Keywords | compiler security, compositionality, cryptography, data flow, design mistakes, design stage, electronic engineering computing, formal verification, formal verification methods, Hardware, hardware description languages, Hardware design languages, hardware designer, hardware overhead, hardware system, hardware vulnerabilities, integrated circuit design, Integrated circuit modeling, integrated circuit testing, language based framework, language-based approach, language-based hardware security verification, malicious logic detection, Measurement, Metrics, potential security vulnerabilities, pre-silicon security assessment, promising solution, pubcrawl, QIF model, QIF-Verilog, quantified information flow model, quantitative information-flow, Registers, resilience, Resiliency, Scalability, security, security of data, security rules, security solutions, Uncertainty, verification process, Verilog type systems, vulnerability analysis, vulnerable logic detection |
| Abstract | 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. |
| DOI | 10.1109/HST.2019.8740840 |
| Citation Key | guo_qif-verilog_2019 |
QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment