Runtime SoC Trust Verification using Integrated Symbolic Execution and Solver

Abstract

Untrusted third-party vendors and manufacturers have raised security concerns in hardware supply chain. Among all existing solutions, formal verification methods provide powerful solutions in detection malicious behaviors at the pre-silicon stage. However, little work have been done towards built-in hardware runtime verification at the post- silicon stage. In this paper, a runtime formal verification framework is proposed to evaluate the trust of hardware during its execution. This framework combines the symbolic execution and SMT solving methods to validate the user defined properties. The proposed framework has been demonstrated on an FPGA platform using a SoC design with untrusted IPs. The experimentation results show that the proposed approach can provide high-level security assurance for hardware at runtime.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 12, 2018
Accession Number
AD1052622

Entities

People

  • Jiaji He
  • Xiaolong Guo
  • Yier Jin

Organizations

  • University of Florida

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Algorithms
  • Case Studies
  • Computational Complexity
  • Cycles
  • Data Transmission
  • Denial Of Service Attack
  • Engineering
  • Equations
  • Fabrication
  • Integrators
  • Intellectual Property
  • Life Cycles
  • Military Research
  • Security
  • Security Protocols
  • Semiconductor Manufacturing
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Cybersecurity.
  • Database Systems and Applications