Towards Property Driven Hardware Security
Authors:
- Wei HuWHWei Hu
- Alric AlthoffAAAlric Althoff
- Armaiti ArdeshirichamAAArmaiti Ardeshiricham
- Ryan KastnerRKRyan Kastner
- 1 December 2016
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 51-56
Abstract
Secure hardware design is a challenging task due to the fact that security properties are difficult or impossible to model and subsequently verify using traditional hardware design tools. The "state of the art" for hardware design security relies heavily on functional verification, manual inspection, and code review to identify security vulnerabilities. This labor intensive process significantly reduces productivity while proving no guarantee that a security flaw will be identified. In this paper, we describe a property driven approach to hardware security, which allows automatic synthesis and verification of both qualitative and quantitative security properties. We address hardware security by enforcing information flow and statistical security properties. By incorporating a new security property specification language, such security properties can be specified, translated and verified using hardware design tools. We present design examples to demonstrate our property driven hardware security solution for proving isolation, detecting timing channel, eliminating hardware Trojan, and enforcing security related statistical properties.Keywords
This publication has 22 references indexed in Scilit:
- On Subnormal Floating Point and Abnormal Timing2015
- Leveraging Gate-Level Properties to Identify Hardware Timing ChannelsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2014
- An exploration of L2 cache covert channels in virtualized environments2011
- Crafting a usable microkernel, processor, and I/O system with strict and provable information flow securityACM SIGARCH Computer Architecture News, 2011
- A case study in hardware Trojan design and implementationInternational Journal of Information Security, 2010
- Secure program execution via dynamic information flow trackingACM SIGOPS Operating Systems Review, 2004
- Language-based information-flow securityIEEE Journal on Selected Areas in Communications, 2003
- Examining smart-card security under the threat of power analysis attacksIEEE Transactions on Computers, 2002
- Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems1996
- A lattice model of secure information flowCommunications of the ACM, 1976