Trusted Module Acquisition Through Proof-Carrying Hardware Intellectual Property.

摘要

By borrowing ideas from the proof carrying code (PCC) in software domain, in this project we introduced the proof carrying hardware intellectual property (PCHIP) framework, which aims to ensure the trustworthiness of third-party hardware IPs utilizing formal methods. We were able to build the fundamental PCHIP framework, enhance its capabilities to be usable for various hardware types with different requirements, e.g. microprocessor IPs or cryptographic cores, and automate parts or all of the extra duties imposed by the PCHIP on hardware IP developers. PCHIP involves these three additional tasks: development of security properties for the design as formal theorems, conversion of the HDL code to the formal representation, and construction of formal proofs for those security theorems. We established a set of security properties which ensure the trustworthiness of microprocessor IPs and developed VeriCoq, which automates the conversion of hardware IPs in Verilog to their equivalent Coq representation. We also built a special PCHIP framework for cryptographic cores, capable of tracking sensitive information through the design and ensure their secureness. Finally, we developed VeriCoq-IFT, which automates all of PCHIP's tasks for this special framework, including conversion of HDL code to formal representation and generation of security theorems and their proofs.