TY - JOUR
T1 - A hardware design language for timing-sensitive information-flow security
AU - Zhang, Danfeng
AU - Wang, Yao
AU - Suh, G. Edward
AU - Myers, Andrew C.
N1 - Publisher Copyright:
Copyright © 2015 ACM.
PY - 2015/4
Y1 - 2015/4
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84951072703&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84951072703&partnerID=8YFLogxK
U2 - 10.1145/2694344.2694372
DO - 10.1145/2694344.2694372
M3 - Article
AN - SCOPUS:84951072703
VL - 50
SP - 503
EP - 516
JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
SN - 1523-2867
IS - 4
ER -