Title

Cycle-Accurate Information Assurance By Proof-Carrying Based Signal Sensitivity Tracing

Abstract

We propose a new information assurance model which can dynamically track the information flow in circuit designs and hence protect sensitive data from malicious leakage. Relying on the Coq proof assistant platform, the new model maps register transfer level (RTL) codes written in hardware description languages (HDLs) into structural Coq representatives by assigning all input, output, and internal signal sensitivity levels. The signal sensitivity levels can be dynamically adjusted after each clock cycle based on proposed signal sensitivity transition rules. The development of data secrecy properties and theorem generation functions makes the translation process from security properties to Coq theorems independent of target circuits and, for the first time, makes it possible to construct a property library, facilitating (semi) automation of the proof. The proposed cycle accurate information assurance scheme is successfully demonstrated on cryptographic circuits with various complexities from a small-scale DES encryption core to a state-of-the-art AES encryption design prohibiting the leakage of sensitive information caused by hardware Trojans inserted in RTL codes. © 2013 IEEE.

Publication Date

9-16-2013

Publication Title

Proceedings of the 2013 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2013

Number of Pages

99-106

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1109/HST.2013.6581573

Socpus ID

84883719198 (Scopus)

Source API URL

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

This document is currently not available here.

Share

COinS