SecChisel: Language and tool for practical and scalable security verification of security-aware hardware architectures

Shuwen Deng, Doğuhan Gümüşoğlu, Wenjie Xiong, Sercan Sari, Y. Serhan Gener, Corine Lu, Onur Demir, Jakub Szefer
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 06 October 2019

Proceedings of the 8th International Workshop on Hardware and Architectural Support for Security and Privacy
Pages 7:1-7:8
Topic(s): security tools
Note(s): information flow
Papers: demoura:tacas:2008

Extends Chisel with security labels to track information flow. Uses the Z3 SMT solver to check but check is based on syntactic structure, not on semantic analysis. That is, it just propagates labels. Suggests this is important for performance.

Sketches several optimisations — I would have liked to have had more detail here. There seem to be several strategies for labelling each module: explicitly label all flops; explicitly label inputs and outputs of module and scan internal connectivity to check for flow; programmer sketches abstract connectivity by specifying which inputs are connected to which outputs as a matrix. It is not clear whether hybrids of these are supported. The paper seems like an early report with many unimplemented features (dynamic labelling, nested modules, Chisel 3 support) and no case study to demonstrate/test/evaluate design choices. Related work discusses a lot of other security related hardware description languages.