Security Specification Mining
Hardware companies conduct extensive testing and verification throughout the design phase, yet errata in the design persist to the final shipped product. Just as is the case with software, bugs in the hardware can create vulnerabilities that are exploitable by malicious software. Security assertions are effective in detecting security vulnerabilities. The question of what to assert – what are the properties that are critical to security – is an open one, and the problem addressed by this project.
Publications
-
Mining Security Critical Linear Temporal Logic Specifications for
Processors
C. Deutschbein, C. Sturton
International Workshop on Microprocessor and SoC Test, Security, and Verification (MTV), 2018. To appear.
-
Identifying Security Critical Properties for the Dynamic Verification of a Processor
R. Zhang, N. Stanley, C. Griggs, A. Chi, C. Sturton
ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2017.
-
SPECS: A Lightweight Runtime Mechanism for Protecting Software from Security Critical Processor Bugs
M. Hicks, C. Sturton, S.T. King, J.M. Smith
ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2015.
Funding
This material is based upon work supported by the National Science Foundation under Grants No. 651276, 1816637. This research is also supported by a Google Faculty Research Award and a University of North Carolina at Chapel Hill Junior Faculty Development Award.