Pre-Silicon Security Verification And Validation: A Formal Perspective

Abstract

Reusable hardware Intellectual Property (IP) based System-on-ChIP (SoC) design has emerged as a pervasive design practice in the industry today. The possibility of hardware Trojans and/or design backdoors hiding in the IP cores has raised security concerns. As existing functional testing methods fall short in detecting unspecified (often malicious) logic, formal methods have emerged as an alternative for validation of trustworthiness of IP cores. Toward this direction, we discuss two main categories of formal methods used in hardware trust evaluation: theorem proving and equivalence checking. Specifically, proof-carrying hardware (PCH) and its applications are introduced in detail, in which we demonstrate the use of theorem proving methods for providing high-level protection of IP cores. We also outline the use of symbolic algebra in equivalence checking, to ensure that the hardware implementation is equivalent to its design specification, thus leaving little space for malicious logic insertion.

Publication Date

7-24-2015

Publication Title

Proceedings - Design Automation Conference

Volume

2015-July

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1145/2744769.2747939

Socpus ID

84944128113 (Scopus)

Source API URL

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

This document is currently not available here.

Share

COinS