A Hardware Design Language for Timing-Sensitive Information-Flow Security
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Mar 14, 2015
- Source ID
- 10.1145/2786763.2694372
Entities
People
- Andrew C. Myers
- Danfeng Zhang
- G. Edward Suh
- Yao Wang
Organizations
- Cornell University
- National Science Foundation
- Office of Naval Research
- United States Air Force