Using security invariant to verify confidentiality in hardware design

Shuyu Kong, Yuanqi Shen, Hai Zhou

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationGLSVLSI 2017 - Proceedings of the Great Lakes Symposium on VLSI 2017
PublisherAssociation for Computing Machinery
Pages487-490
Number of pages4
ISBN (Electronic)9781450349727
DOIs
StatePublished - May 10 2017
Event27th Great Lakes Symposium on VLSI, GLSVLSI 2017 - Banff, Canada
Duration: May 10 2017May 12 2017

Publication series

NameProceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI
VolumePart F127756

Other

Other27th Great Lakes Symposium on VLSI, GLSVLSI 2017
CountryCanada
CityBanff
Period5/10/175/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