Trusted Module Acquisition Through Proof-Carrying Hardware Intellectual Property
Final rept. 24 Feb 2012-23 Feb 2015
TEXAS UNIV AT DALLAS RICHARDSON DEPT OF ELECTRICAL ENGINEERING
Pagination or Media Count:
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 PCHIPs tasks for this special framework, including conversion of HDL code to formal representation and generation of security theorems and their proofs.
- Computer Programming and Software
- Computer Hardware
- Computer Systems Management and Standards