|
The task of designing modern hardware that is impervious to any and every security attack is almost impossible to achieve. It is extremely hard to ensure that these complex, multi-billion transistor systems are functionally correct, let alone secure. Thus, it should not be surprising that there are a large and growing number of attacks that target hardware vulnerabilities. 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 does not scale, it significantly reduces productivity, and provides no guarantee that a security flaw will be identified. Continuing with the status quo will undoubtedly leave hardware designs susceptible to attacks manifested through hardware, firmware, and software vulnerabilities. This project develops a property driven approach to hardware security, which enables automatic verification of security properties on a hardware design.
The project encompasses three major research goals: creating expressive security property languages, building comprehensive models that analyze the security of a hardware design, and generating tools that can verify security properties in an efficient and scalable manner. The investigators address these challenges by developing models that enable the specification of a wide variety of security properties. The project builds a novel security property specification languages leveraging these models, and develops new techniques that enable the verification of these properties using existing formal solvers, simulation environments, and emulation platforms. Finally, they address the usability of this property driven approach by verifying security properties on different hardware designs.
|
SaTC: STARSS: Small: Property Driven Hardware Security