Runtime SoC Trust Verification using Integrated Symbolic Execution and Solver
University of Florida Department of Electrical and Computer Engineering Gainesville United States
Pagination or Media Count:
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.