Data Secrecy Protection Through Information Flow Tracking In Proof-Carrying Hardware Ip - Part Ii: Framework Automation

Keywords

Hardware trust; information flow tracking; proof-carrying code; proof-carrying hardware IP

Abstract

Part II of this paper series focuses on automation of the extended proof-carrying hardware intellectual property (PCHIP) framework for data secrecy protection in third-party IPs, which was presented in part I. Specifically, we introduce: 1) VeriCoq-IFT, an automated PCHIP framework for information flow policies and 2) VeriCoq-H, a hierarchy-preserving Verilog-to-Coq converter. VeriCoq-IFT aims to: 1) automate the process of converting designs from an HDL to the Coq formal language; 2) generate security property theorems ensuring compliance with information flow policies; 3) construct proofs for such theorems; and 4) check their validity in a design, with minimal user intervention. VeriCoq-H, on the other hand, seeks to convert the entire functionality of a Verilog design to its Coq representation while preserving design hierarchy. It facilitates the development of hierarchical proofs and enables the construction of hybrid module libraries containing the HDL code and the corresponding reusable lemmas for each module. Applicability of our automated VeriCoq-IFT framework is demonstrated by evaluating trustworthiness of two DES encryption circuits and several genuine and Trojan-infested advanced encryption standard (AES) designs, along with the utility of VeriCoq-H in preventing malicious modification of sensitive data, such as the secret key of an encryption circuit.

Publication Date

10-1-2017

Publication Title

IEEE Transactions on Information Forensics and Security

Volume

12

Issue

10

Number of Pages

2430-2443

Document Type

Article

Personal Identifier

scopus

DOI Link

https://doi.org/10.1109/TIFS.2017.2707327

Socpus ID

85029215077 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/85029215077

This document is currently not available here.

Share

COinS