Toward automatic proof generation for information flow policies in third-party hardware IP

The proof carrying hardware intellectual property (PCHIP) framework ensures trustworthiness by developing proofs for security properties designed to prevent introduction of malicious behaviors via third-party hardware IP. However, converting a design to a formal representation and developing proofs for the desired security properties is a cumbersome task for IP developers and requires extra knowledge of formal reasoning methods, proof development and proof checking. While security properties are generally specific to each design, information flow policies are a set of policies which ensure that no secret information is leaked through untrusted channels, and are mainly applicable to the designs which manipulate secret and sensitive data. In this work, we introduce the VeriCoq-IFT framework which aims to (i) automate the process of converting designs from HDL to the Coq formal language, (ii) generate security property theorems ensuring information flow policies, (iii) construct proofs for such theorems, and (iv) check their validity for the design, with minimal user intervention. We take advantage of Coq proof automation facilities in proving the generated theorems for enforcing these policies and we demonstrate the applicability of our automated framework on two DES encryption circuits. By providing essential information, the trustworthiness of these circuits in terms of information flow policies is verified automatically. Any alteration of the circuit description against information flow policies causes proofs to fail. Our methodology is the first but essential step in the adoption of PCHIP as a valuable method to authenticate the trustworthiness of third party hardware IP with minimal extra effort.