Cryptology ePrint Archive: Report 2017/193

SecChisel: Language and Tool for Practical and Scalable Security Verification of Security-Aware Hardware Architectures

Shuwen Deng and Doğuhan Gümüşoğlu and Wenjie Xiong and Y. Serhan Gener and 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.

Category / Keywords: implementation / hardware security verification

Date: received 25 Feb 2017

Contact author: jakub szefer at yale edu

Available format(s): PDF | BibTeX Citation

Version: 20170228:193327 (All versions of this report)

Short URL:

Discussion forum: Show discussion | Start new discussion

[ Cryptology ePrint archive ]