Scalable Soc Trust Verification Using Integrated Theorem Proving And Model Checking

Abstract

The wide usage of hardware Intellectual Property (IP) cores and software programs from untrusted vendors have raised security concerns for system designers. Existing solutions for detecting and preventing software attacks do not usually consider the presence of malicious logic in hardware. Similarly, hardware solutions for detecting Trojans and/or design backdoors do not consider the software running on it. Formal methods provide powerful solutions in detecting malicious behaviors in both hardware and software. However, they suffer from scalability issues and cannot be easily used for large-scale computer systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of computer systems constructed from untrusted third-party software and hardware resources. This framework combines an automated model checker with an interactive theorem prover for proving system-level security properties. We evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with considerable reduction in effort. Our method systematically reduces the effort required for verifying the program running on the System-on-Chip (SoC) compared to traditional interactive theorem proving methods.

Publication Date

6-20-2016

Publication Title

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

Number of Pages

124-129

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

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

Socpus ID

84979619679 (Scopus)

Source API URL

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

This document is currently not available here.

Share

COinS