The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
A Hardware Design Language for Timing-Sensitive Information-Flow Security
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
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.
@article{zhang2015hardware,
title = {A Hardware Design Language for Timing-Sensitive Information-Flow Security},
author = {Danfeng Zhang and Yao Wang and G. Edward Suh and Andrew C. Myers},
year = {2015},
journal = {ACM SIGPLAN Notices},
publisher = {Association for Computing Machinery},
volume = {50},
number = {4},
pages = {503--516},
doi = {10.1145/2775054.2694372},
}