Using security invariant to verify confidentiality in hardware design

Shuyu Kong; Yuanqi Shen; Hai Zhou

doi:10.1145/3060403.3060456

Using security invariant to verify confidentiality in hardware design

Shuyu Kong, Yuanqi Shen, Hai Zhou

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Scopus citations

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	https://doi.org/10.1145/3060403.3060456
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

Access to Document

10.1145/3060403.3060456

Cite this

@inproceedings{036c94ce38be49a8ac58a45304de1802,

title = "Using security invariant to verify confidentiality in hardware design",

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.",

author = "Shuyu Kong and Yuanqi Shen and Hai Zhou",

note = "Publisher Copyright: {\textcopyright} 2017 ACM.; 27th Great Lakes Symposium on VLSI, GLSVLSI 2017 ; Conference date: 10-05-2017 Through 12-05-2017",

year = "2017",

month = may,

day = "10",

doi = "10.1145/3060403.3060456",

language = "English (US)",

series = "Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI",

publisher = "Association for Computing Machinery",

pages = "487--490",

booktitle = "GLSVLSI 2017 - Proceedings of the Great Lakes Symposium on VLSI 2017",

}

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. Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI, vol. Part F127756, Association for Computing Machinery, pp. 487-490, 27th Great Lakes Symposium on VLSI, GLSVLSI 2017, Banff, Canada, 5/10/17. https://doi.org/10.1145/3060403.3060456

Using security invariant to verify confidentiality in hardware design. / Kong, Shuyu; Shen, Yuanqi; Zhou, Hai.
GLSVLSI 2017 - Proceedings of the Great Lakes Symposium on VLSI 2017. Association for Computing Machinery, 2017. p. 487-490 (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI; Vol. Part F127756).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Using security invariant to verify confidentiality in hardware design

AU - Kong, Shuyu

AU - Shen, Yuanqi

AU - Zhou, Hai

PY - 2017/5/10

Y1 - 2017/5/10

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85021216543&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85021216543&partnerID=8YFLogxK

U2 - 10.1145/3060403.3060456

DO - 10.1145/3060403.3060456

M3 - Conference contribution

AN - SCOPUS:85021216543

T3 - Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI

SP - 487

EP - 490

BT - GLSVLSI 2017 - Proceedings of the Great Lakes Symposium on VLSI 2017

PB - Association for Computing Machinery

T2 - 27th Great Lakes Symposium on VLSI, GLSVLSI 2017

Y2 - 10 May 2017 through 12 May 2017

ER -

Using security invariant to verify confidentiality in hardware design

Abstract

Publication series

Other

Funding

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this