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.
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)
ACM
Pages 503-516
2015
Topic(s): security
Note(s): hardware, information flow
Papers: demoura:tacas:2008
ACM
Pages 503-516
2015
Topic(s): security
Note(s): hardware, information flow
Papers: demoura:tacas:2008