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

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

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

34 Scopus citations

Abstract

Information security can be compromised by leakage via low-level 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)
Title of host publicationASPLOS 2015 - 20th International Conference on Architectural Support for Programming Languages and Operating Systems
PublisherAssociation for Computing Machinery
Pages503-516
Number of pages14
ISBN (Electronic)9781450328357
DOIs
StatePublished - Mar 14 2015
Event20th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2015 - Istanbul, Turkey
Duration: Mar 14 2015Mar 18 2015

Publication series

NameInternational Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
Volume2015-January

Other

Other20th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2015
CountryTurkey
CityIstanbul
Period3/14/153/18/15

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Hardware and Architecture

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