Ensuring Hardware Robustness via Security Verification
| dc.contributor.advisor | Basu, Kanad | |
| dc.contributor.advisor | Schmidtke, David | |
| dc.contributor.committeeMember | Bhatia, Dinesh | |
| dc.contributor.committeeMember | Makris, Yiorgos | |
| dc.contributor.committeeMember | Saquib, Mohammad | |
| dc.creator | Meng, Xingyu 1993- | |
| dc.creator.orcid | 0000-0001-5787-0101 | |
| dc.date.accessioned | 2024-03-07T22:44:01Z | |
| dc.date.available | 2024-03-07T22:44:01Z | |
| dc.date.created | 2023-12 | |
| dc.date.issued | December 2023 | |
| dc.date.submitted | December 2023 | |
| dc.date.updated | 2024-03-07T22:44:01Z | |
| dc.description.abstract | System-on-Chips (SoCs) play a pivotal role in modern computing systems, integrating multiple Intellectual Property (IP) cores to deliver diverse functionalities. However, this integration presents unique security challenges that can result in vulnerabilities escaping the verification phase and becoming potential exploits. Moreover, the integration of commercial off-the-shelf (COTS) components into system designs provides cost-effective solutions but introduces the risk of hidden malicious hardware. On the other hand, asynchronous events in complex SoC design introduce challenges for security verification. Furthermore, Network-on-Chip (NoC) architectures introduce new vulnerabilities during message transmission across on-chip networks. Although security properties are introduced to address these vulnerabilities, generating security properties for SoCs can be a daunting task, typically requiring extensive developer expertise and time. This dissertation extends and explores various approaches to current hardware verification in multiple aspects. First, we introduce RTL-ConTest, a Register Transfer Level (RTL) security vulnerability detection algorithm, that extracts critical process flows from a design and executes RTL-level Concolic testing to generate security test cases for identifying critical exploits. Second, we address the asynchronous resets by extending the concept of control flow graph (CFG) and extraction of reset-controlled events while avoiding combinatorial explosion. Third, by utilizing CFG extraction and security properties, we develop a framework for systematic detection of security violations in NoC designs resulting from vulnerabilities in NoC communication through formal state exploration. Fourth, We propose an information tracking framework to identify potential information flow violations in COTS integrated circuits by analyzing their designs and demonstrating their effectiveness in experimental results. Lastly, we introduce a language-based machine-learning framework that extracts essential security information from processor documentation and converts them into security constraints at the RTL level, enhancing the robustness and efficiency of security property generation. | |
| dc.format.mimetype | application/pdf | |
| dc.identifier.uri | ||
| dc.identifier.uri | https://hdl.handle.net/10735.1/10013 | |
| dc.language.iso | English | |
| dc.subject | Engineering, Electronics and Electrical | |
| dc.title | Ensuring Hardware Robustness via Security Verification | |
| dc.type | Thesis | |
| dc.type.material | text | |
| thesis.degree.college | School of Engineering and Computer Science | |
| thesis.degree.department | Computer Engineering | |
| thesis.degree.grantor | The University of Texas at Dallas | |
| thesis.degree.name | PHD |
Files
Original bundle
1 - 1 of 1