SecVerilog: Verilog + Information Flow

SecVerilog is a new hardware description language (HDL) with fine-grained information flow control. SecVerilog extends Verilog with annotations that support comprehensive, precise reasoning about information flows, including flows via timing, at compile time. The benefit is that hardware designs can be formally verified mostly as-is, with little run-time overhead.

SecVerilog fits into a typical design flow very well, as demonstrated in the figure above. As input, SecVerilog takes Verilog code with security labels (e.g., {D1}, {D2} and {L}). These labels specify the information flow policy to be verified on a hardware design. Once the verification succeeds, security labels are removed, resulting in standard Verilog code. Such Verilog code is then used in a typical hardware design flow. The verified hardware provably obeys the information flow policy specified in the original SecVerilog code, guaranteed by the type system of SecVerilog.

A distinguishing feature of SecVerilog is the support of dependent labels. Dependent labels allow hardware resources to be shared across security domains. In the two-input mux example shown in the figure above, the security domain of out depends on the run-time value of sel: the domain is D1 when sel is 0, and D2 when sel is 1. Such restrictions can be concisely specified by a dependent label {Domain sel}, where Domain is a function from values to labels (defined in a separate file).

By building a secure MIPS processor and its caches, we showed that SecVerilog makes it possible to build complex hardware designs with verified security, yet with low overhead in time, space, and hardware designer effort.


Related publications

Project members


The development of SecVerilog has been supported by Office of Naval Research grant N00014-13-1-0089, MURI grant FA9550-12-1- 0400, Air Force grant FA8750-11-2-0025, and by National Science Foundation grants CNS-0746913, CCF-0905208, CCF-0964409, and CNS-1513797. .