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.