By: Xiaolong Guo and Yier Jin
Stage: RTL
Summary
- A comprehensive Proof-Carrying Hardware (PCH) based system level formal solution to evaluate the hardware trust and to further protect the entire hardware and software system.
- Combines an automated model checker with an interactive theorem prover to reduce the time for proving system-level security properties of SoC’s.
- Fill in the semantic gap of the hardware-software boundary, eliminate the scalablity issue, and verify the application on runtime.
Contact
Input/Output Interface
- Input: Assemble code and Hardware Design – VHDL program
- Output: Whether there is Trojan inserted in the given system
Dependencies
- Coq: https://coq.inria.fr/
- VHD2CA: http://www.fit.vutbr.cz/~smrcka/tools/vhd2ca/
- Cadence IFV: https://www.cadence.com/content/dam/cadence-www/global/en_US/documents/tools/system-design-verification/incisive-formal-verifier-ds.pdf
References
Guo, Xiaolong; Dutta, Raj Gautam; He, Jiaji; Jin, Yier
PCH framework for IP runtime security verification Proceedings Article
In: 2017 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), pp. 79-84, IEEE, 2017.
@inproceedings{Guo2017b,
title = {PCH framework for IP runtime security verification},
author = {Xiaolong Guo and Raj Gautam Dutta and Jiaji He and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2017pch.pdf},
doi = {10.1109/AsianHOST.2017.8353999},
year = {2017},
date = {2017-12-02},
booktitle = {2017 Asian Hardware Oriented Security and Trust Symposium (AsianHOST)},
pages = {79-84},
publisher = {IEEE},
abstract = {Untrusted third-party vendors and manufacturers have raised security concerns in the hardware supply chain. Among all existing solutions, formal verification methods provide powerful solutions in the detection of malicious behaviors at the pre-silicon stage. However, little work has 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 symbolic execution and SAT solving methods to validate the user-defined properties. The proposed framework has been demonstrated on an FPGA platform using an SoC design with untrusted IPs. The experimentation results show that the proposed approach can provide high-level security assurance for hardware at runtime.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Untrusted third-party vendors and manufacturers have raised security concerns in the hardware supply chain. Among all existing solutions, formal verification methods provide powerful solutions in the detection of malicious behaviors at the pre-silicon stage. However, little work has 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 symbolic execution and SAT solving methods to validate the user-defined properties. The proposed framework has been demonstrated on an FPGA platform using an SoC design with untrusted IPs. The experimentation results show that the proposed approach can provide high-level security assurance for hardware at runtime.
Guo, Xiaolong; Dutta, Raj Gautam; Mishra, Prabhat; Jin, Yier
Automatic Code Converter Enhanced PCH Framework for SoC Trust Verification Journal Article
In: IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 25, no. 12, pp. 3390-3400, 2017.
@article{Guo2017,
title = {Automatic Code Converter Enhanced PCH Framework for SoC Trust Verification},
author = {Xiaolong Guo and Raj Gautam Dutta and Prabhat Mishra and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2017automatic.pdf},
doi = {10.1109/TVLSI.2017.2751615},
year = {2017},
date = {2017-12-01},
journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
volume = {25},
number = {12},
pages = {3390-3400},
abstract = {The wide usage of hardware intellectual property cores from untrusted vendors has raised security concerns for system designers. Existing solutions for functionality testing and verification do not usually consider the presence of malicious logic in hardware. Formal methods provide powerful solutions for detecting malicious behaviors in hardware. However, they suffer from scalability issues and cannot be easily used for large-scale computing systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of system-on-chip (SoC) constructed from untrusted third-party hardware resources. This framework combines an automated model checker with an interactive theorem prover to reduce the time for proving the system-level security properties of SoCs. Another factor contributing to the scalability issue is the effort required for manual conversion of the hardware design from register transfer level (RTL) code to a domain-specific language prior to verification. Consequently, we develop an automatic code converter for translating VHSIC hardware description language (VHDL) to Formal-HDL, which is a domain-specific language for representing hardware designs in the language of Coq. To demonstrate the effectiveness of our integrated verification framework and automated code conversion tool, we evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with a considerable reduction in verification effort.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The wide usage of hardware intellectual property cores from untrusted vendors has raised security concerns for system designers. Existing solutions for functionality testing and verification do not usually consider the presence of malicious logic in hardware. Formal methods provide powerful solutions for detecting malicious behaviors in hardware. However, they suffer from scalability issues and cannot be easily used for large-scale computing systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of system-on-chip (SoC) constructed from untrusted third-party hardware resources. This framework combines an automated model checker with an interactive theorem prover to reduce the time for proving the system-level security properties of SoCs. Another factor contributing to the scalability issue is the effort required for manual conversion of the hardware design from register transfer level (RTL) code to a domain-specific language prior to verification. Consequently, we develop an automatic code converter for translating VHSIC hardware description language (VHDL) to Formal-HDL, which is a domain-specific language for representing hardware designs in the language of Coq. To demonstrate the effectiveness of our integrated verification framework and automated code conversion tool, we evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with a considerable reduction in verification effort.
Guo, Xiaolong; Dutta, Raj Gautam; Mishra, Prabhat; Jin, Yier
Scalable SoC trust verification using integrated theorem proving and model checking Proceedings Article
In: 2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 124-129, HOST IEEE, McLean, VA, USA , 2016.
@inproceedings{Guo2016b,
title = {Scalable SoC trust verification using integrated theorem proving and model checking},
author = {Xiaolong Guo and Raj Gautam Dutta and Prabhat Mishra and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2016scalable.pdf},
doi = {10.1109/HST.2016.7495569},
year = {2016},
date = {2016-03-15},
booktitle = {2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)},
pages = {124-129},
publisher = {IEEE},
address = {McLean, VA, USA },
organization = {HOST },
series = {HOST 16},
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 a 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.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
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 a 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.
Guo, Xiaolong; Dutta, Raj Gautam; Jin, Yier
Eliminating the Hardware-Software Boundary: A Proof-Carrying Approach for Trust Evaluation on Computer Systems Journal Article
In: IEEE Transactions on Information Forensics and Security (TIFS), vol. 12, no. 2, pp. 405-417, 2016.
@article{Guo2016,
title = {Eliminating the Hardware-Software Boundary: A Proof-Carrying Approach for Trust Evaluation on Computer Systems},
author = {Xiaolong Guo and Raj Gautam Dutta and Yier Jin},
url = {http://cadforassurance.org/wp-content/uploads/xiaolong2016eliminating.pdf},
doi = {10.1109/TIFS.2016.2621999},
year = {2016},
date = {2016-02-01},
journal = {IEEE Transactions on Information Forensics and Security (TIFS)},
volume = {12},
number = {2},
pages = {405-417},
abstract = {The wide usage of hardware intellectual property (IP) cores and software programs from untrusted third-party vendors have 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 that 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.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The wide usage of hardware intellectual property (IP) cores and software programs from untrusted third-party vendors have 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 that 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.
Acknowledgments
- This work was partially supported by National Science Foundation (CNS-1319105), Army Research Office (W911NF-17-1-0477), Cisco and National Natural Science Foundation of China (61376032)