Hardware Trojans hidden in RTL don't cares — Automated insertion and prevention methodologies
- 1 October 2015
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2015 IEEE International Test Conference (ITC)
Abstract
Don't cares in RTL code have long plagued chip verification due to hard-to-diagnose “X-bugs” resulting from ambiguous X simulation semantics, yet prevail in modern designs because of enormous opportunities for area/performance/power optimization during synthesis. We analyze don't cares specified at the RTL level from a security perspective and propose a novel class of Hardware Trojans which leak internal circuit node values using only existing design don't cares. Detection of this Trojan class is impossible using either functional simulation/verification or a perfect sequential equivalence checker. We then provide a formal automated X-analysis technique which both prevents the insertion of this new Trojan type and also has the potential to uncover accidental X-bugs as well. We provide several examples, including an Elliptic Curve Processor, illustrating both Trojan insertion and our prevention technique.Keywords
This publication has 13 references indexed in Scilit:
- FIGHT-MetricPublished by Association for Computing Machinery (ACM) ,2014
- Hardware Trojan Horses in Cryptographic IP CoresPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2013
- VeriTrustPublished by Association for Computing Machinery (ACM) ,2013
- Secure Hardware IPs by Digital WatermarkPublished by Springer Science and Business Media LLC ,2011
- SAT-Based Model Checking without UnrollingLecture Notes in Computer Science, 2011
- A Survey of Hardware Trojan Taxonomy and DetectionIEEE Design & Test of Computers, 2010
- The Hunt For The Kill SwitchIEEE Spectrum, 2008
- Improving SAT-based bounded model checking by means of BDD-based approximate traversalsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Efficient use of large don't cares in high-level and logic synthesisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal Equivalence Checking and Design DebuggingPublished by Springer Science and Business Media LLC ,1998