A hardware design language for timing-sensitive information flow security

Danfeng Zhang, Yao Wang, G. Edward Suh, Andrew C. Myers
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 06 October 2019

ACM SIGARCH Computer Architecture News 43(1)
Pages 503-516
Topic(s): security
Note(s): hardware, information flow
Papers: demoura:tacas:2008

Extends Verilog with security labels and declassification. Labels can be static or dynamic and are tracked using a modified type system with some tricks to improve precision (related to implicit flows). Analysis is (of course) timing sensitive so timing channels are automatically handled. Constraints generated by type system are solved using the Z3 SMT solver. Evaluated on a MIPS CPU with two additional instructions to set timing labels and PPA evaluated (little impact). Benchmarks include MiBench and OpenSSL. Not clear if any form of label polymorphism is supported.