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; Y.  Serhan Gener; Onur Demir; Jakub Szefer

Paper 2017/193

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, Y. Serhan Gener, Onur Demir, and Jakub Szefer

Abstract

Due to lack of practical and scalable security verification tools and methodologies, very few of the existing hardware-software security architectures have been thoroughly checked at the design time. To address this issue, our project develops a security verification methodology that is applicable to different hardware-software security architectures during the design phase. The verification framework aims to prove that a system holds desired properties with respect to not just functionality but also security; and we mainly focus on information flow and non-interference properties for verification. Using these properties, confidentiality and integrity of the sensitive data can be checked at design time. The proposed verification framework is built upon Chisel hardware construction language. By extending the Chisel language and tools, we created SecChisel. Ongoing work is focused on implementing SecChisel on top of Chisel~3 and realisation of the static and dynamic security labels.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint. MINOR revision.
Keywords: hardware security verification
Contact author(s): jakub szefer @ yale edu
History: 2017-02-28: received
Short URL: https://ia.cr/2017/193
License: CC BY

BibTeX

@misc{cryptoeprint:2017/193,
      author = {Shuwen Deng and Doğuhan Gümüşoğlu and Wenjie Xiong and Y.  Serhan Gener and Onur Demir and Jakub Szefer},
      title = {{SecChisel}: Language and Tool for Practical and Scalable Security Verification of Security-Aware Hardware Architectures},
      howpublished = {Cryptology {ePrint} Archive, Paper 2017/193},
      year = {2017},
      url = {https://eprint.iacr.org/2017/193}
}