A hardware design language for timing-sensitive information-flow security

Danfeng Zhang, Yao Wang, G. Edward Suh, Andrew C. Myers

Research output: Contribution to journalArticlepeer-review

68 Scopus citations

Abstract

Information security can be compromised by leakage via lowlevel hardware features. One recently prominent example is cache probing attacks, which rely on timing channels created by caches. We introduce a hardware design language, SecVerilog, which makes it possible to statically analyze information flow at the hardware level. With SecVerilog, systems can be built with verifiable control of timing channels and other information channels. SecVerilog is Verilog, extended with expressive type annotations that enable precise reasoning about information flow. It also comes with rigorous formal assurance: we prove that SecVerilog enforces timing-sensitive noninterference and thus ensures secure information flow. By building a secure MIPS processor and its caches, we demonstrate that SecVerilog makes it possible to build complex hardware designs with verified security, yet with low overhead in time, space, and HW designer effort.

Original languageEnglish (US)
Pages (from-to)503-516
Number of pages14
JournalACM SIGPLAN Notices
Volume50
Issue number4
DOIs
StatePublished - Apr 2015

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Fingerprint Dive into the research topics of 'A hardware design language for timing-sensitive information-flow security'. Together they form a unique fingerprint.

Cite this