Collaborative Research: SaTC: CORE: Medium: Hardware Security Insights: Analyzing Hardware Designs to Understand and Assess Security Weaknesses and Vulnerabilities

This project’s goal is to develop better methods for understanding how information flows in computer hardware designs, and thus increase their security. The microprocessors, wireless modems, graphics processing units, and other hardware components at the heart of all computing devices are designed by engineers using low-level hardware description languages. These designs are complex, making it difficult to reason about security vulnerabilities that may allow attackers to extract valuable secret information like cryptographic keys and personally identifiable information. Hardware security verification aims to identify hardware weaknesses, patch potential vulnerabilities, and mitigate the harm of attacks. Understanding how information flows in hardware designs can help verification engineers to assess whether secret data can be extracted by an attacker and to develop designs that prevent those vulnerable flows. The project is structured around three main aims that together will lead to improved tools for insights around hardware information flow tracking. The first aim is to automate the generation of information-flow properties, which can then be verified by existing tools. The second is to develop testbenches that fully exercise possible information flows through a design, using angelic execution oracles designed to maximize coverage of possible information flows. The third is to develop a new “hyperflow analysis” framework that provides both analytic representations to support algorithms for hardware design and verification, and visual representations that help verification engineers explore hardware vulnerabilities through an information-flow lens. The work will involve a number of undergraduate and graduate students, contributing to the development of the computer security workforce. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.