Eliminating The Hardware-Software Boundary: A Proof-Carrying Approach For Trust Evaluation On Computer Systems

Keywords

Coq proof assistant; Cross-layer protection; Formal verification; Hardware trust; Proof-carrying code; Proof-carrying hardware

Abstract

The wide usage of hardware intellectual property (IP) cores and software programs from untrusted third-party vendors has raised security concerns for computer system designers. The existing approaches, designed to ensure the trustworthiness of either the hardware IP cores or to verify software programs, rarely secure the entire computer system. The semantic gap between the hardware and the software lends to the challenge of securing computer systems. In this paper, we propose a new unified framework to represent both the hardware infrastructure and the software program in the same formal language. As a result, the semantic gap between the hardware and the software is bridged, enabling the development of system-level security properties for the entire computer system. Our unified framework uses a cross-domain formal verification method to protect the entire computer system within the scope of proof-carrying hardware. The working procedure of the unified framework is demonstrated with a sample embedded system which includes an 8051 microprocessor and an RC5 encryption program. In our demonstration, we show that the embedded system is trusted if the system level security properties are provable. Supported by the unified framework, the system designers/integrators will be able to formally verify the trustworthiness of the computer system integrated with hardware and software both from untrusted third-party vendors.

Publication Date

2-1-2017

Publication Title

IEEE Transactions on Information Forensics and Security

Volume

12

Issue

2

Number of Pages

405-417

Document Type

Article

Personal Identifier

scopus

DOI Link

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

Socpus ID

85013420132 (Scopus)

Source API URL

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

This document is currently not available here.

Share

COinS