Abstract
Due to the increasing complexity of design process, outsourcing, and use of third-party blocks, it becomes harder and harder to prevent Trojan insertion and other malicious design modifications. In this paper, we propose to deploy security invariant as carried proof to prevent and detect Trojans and malicious attacks and to ensure the security of hardware design. Non-interference with down-grading policy is checked for confidentiality. Contrary to existing approaches by type checking, we develop a method to model-check a simple safety property on a composed machine. Down-grading is handled in a better way in model-checking and the effectiveness of our approach is demonstrated on various Verilog benchmarks.
Original language | English (US) |
---|---|
Title of host publication | GLSVLSI 2017 - Proceedings of the Great Lakes Symposium on VLSI 2017 |
Publisher | Association for Computing Machinery |
Pages | 487-490 |
Number of pages | 4 |
ISBN (Electronic) | 9781450349727 |
DOIs | |
State | Published - May 10 2017 |
Event | 27th Great Lakes Symposium on VLSI, GLSVLSI 2017 - Banff, Canada Duration: May 10 2017 → May 12 2017 |
Publication series
Name | Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI |
---|---|
Volume | Part F127756 |
Other
Other | 27th Great Lakes Symposium on VLSI, GLSVLSI 2017 |
---|---|
Country/Territory | Canada |
City | Banff |
Period | 5/10/17 → 5/12/17 |
Funding
This work is partially supported by NSF under CNS-1651695 and CNS-1441695, and by SRC under 2014-TS-2559.
ASJC Scopus subject areas
- General Engineering