Title: Hardware Security and Trust Verification
Abstract: System-on-Chip (SoC) is the brain behind computing and communication in a wide variety of systems. Reusable hardware Intellectual Property (IP) based System-on-Chip (SoC) design has emerged as a pervasive design practice in the industry to dramatically reduce design and verification cost while meeting aggressive time-to-market constraints. Growing reliance on these pre-verified hardware IPs, often gathered from untrusted third-party vendors, severely affects the security and trustworthiness of SoC computing platforms. These third-party IPs may come with deliberate malicious implants to incorporate undesired functionality (e.g., hardware Trojans), undocumented test/debug interface working as hidden backdoor, or other integrity issues. It is extremely difficult to verify integrity and trust of hardware IPs due to several reasons including (a) lack of a golden reference model or incomplete specification, (b) exponential space of diverse types of complex IPs and IP-specific vulnerabilities, (c) lack of automated and scalable CAD tools for IP trust verification, and (d) lack of security metrics to measure the security robustness of a given design or mitigation technique. While functional validation has received significant attention over the years, it is critical to perform “security and trust verification” for designing trustworthy systems.
This tutorial will provide a comprehensive overview of both fundamental concepts and recent advances in hardware security and trust validation using simulation-based approaches, formal methods as well as side-channel analysis. Specifically, the tutorial will consist of four parts. The first part will introduce security vulnerabilities (threats) and various challenges associated with trust validation of hardware IPs. It will highlight recent advances in developing trust metrics and benchmarks. The second part will cover assertion-based security validation utilizing automated generation of security assertions. It will also cover automated test generation techniques for activation of security assertions. The third part will describe how formal verification techniques (including model checking, SAT solving, theorem proving and equivalence checking) can be effectively utilized for validation of hardware security vulnerabilities. The fourth part will discuss how side-channel analysis can be effectively utilized to detect malicious implants. It will conclude with a discussion on integration of security verification in existing functional validation methodology.
This tutorial will be based on both the prior work of the presenter and the work of other prominent researchers in this field. It will cover theoretical aspects as well as industrial practices with real-life case studies. Following is the organization of the tutorial that consists of four major components.
Part I: Introduction and Motivation
- Security and trust validation challenges (why functional validation is not enough)
- Development of threat models, trust metrics and benchmarks
Part II: Simulation-based Security and Trust Validation
- Automated vulnerability analysis of RTL models
- Assertion-based validation of security vulnerabilities
- Scalable test generation for activation of malicious implants
Part III: IP Trust Verification using Formal Methods
- Model checking to verify unwanted scenarios (security properties)
- Equivalence checking to ensure nothing more, nothing less.
- Scalable trust verification using theorem proving
Part IV: Hardware Trojan Detection using Side-Channel Analysis
- Logic testing versus side-channel analysis for detecting malicious implants
- Trojan detection using dynamic current (power), path delay, and electromagnetic emanations
Part V: Conclusions and Future Directions
- Seamless integration of security verification techniques in existing functional validation flow
- Future trends and research directions
This tutorial is primarily targeted towards validation and verification engineers interested in security and trust of integrated circuits and systems. This tutorial will also attract designers, tool developers, managers, and researchers working in the broad area of trustworthy system design.
Length and Format
The tutorial would be ideal as a full day presentation (6-8 hours). It can be reduced to half day, if needed. It will have both lecture and hands-on components. The case studies slides will provide step-by-step instructions for running specific software (e.g., RTL vulnerability analysis) that the attendees can run real-time or later at their convenience.
An early version of this tutorial was offered in IACR Cryptographic Hardware and Embedded Systems (CHES), 2019. It was attended by 40-50 participants.
Prabhat Mishra is a Professor in the Department of Computer and Information Science and Engineering and a UF Research Foundation Professor at the University of Florida. His research interests include embedded and cyber-physical systems, hardware security and trust, energy-aware computing, formal verification, system-on-chip validation, and post-silicon debug. He received his Ph.D. in Computer Science from the University of California at Irvine in 2004. Prior to joining University of Florida, he spent several years in various companies including Intel, Motorola, Sasken, Synopsys and Texas Instruments. He has published 8 books, 35 book chapters, 21 patents/copyrights, and more than 200 research articles in premier international journals and conferences. His research has been recognized by several awards including the NSF CAREER Award from the National Science Foundation, IBM Faculty Award, three Best Paper Awards (ISQED’16, VLSID’11 and CODES+ISSS’03) as well as seven Best Paper Nominations (DATE’19, ASPDAC’17, NANOARCH’13, VLSI’13, DATE’12, DAC’09, VLSI’09), and EDAA Outstanding Dissertation Award from the European Design Automation Association. Prof. Mishra currently serves as an Associate Editor of IEEE Transactions on VLSI Systems and ACM Transactions of Embedded Computing Systems. He has served as the Deputy Editor-in-Chief of IET Computer & Digital Techniques, and as an Associate Editor of ACM Transactions on Design Automation of Electronic Systems, and IEEE Design & Test, and Springer Journal of Electronic Testing. He is an IEEE Fellow and an ACM Distinguished Scientist.