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 | Canada |
| City | Banff |
| Period | 5/10/17 → 5/12/17 |
ASJC Scopus subject areas
- Engineering(all)
Fingerprint Dive into the research topics of 'Using security invariant to verify confidentiality in hardware design'. Together they form a unique fingerprint.
Cite this
Kong, S., Shen, Y., & Zhou, H. (2017). Using security invariant to verify confidentiality in hardware design. In GLSVLSI 2017 - Proceedings of the Great Lakes Symposium on VLSI 2017 (pp. 487-490). (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI; Vol. Part F127756). Association for Computing Machinery. https://doi.org/10.1145/3060403.3060456