Formal Methods for Hardware Security

Hardware security exploits have been in the spotlight since the announcement of the infamous Spectre and Meltdown exploits. These attacks allow an adversarial process to access and leak confidential data by abusing cache pollution that can result from speculative executions. Since their release, several other speculation-based attacks have been reported. To design hardware and software systems that are more secure, it is clear that automated security verification techniques for detecting exploitable hardware behaviors is an important step. In this work, I am using formal analysis techniques to detect vulnerabilities in hardware components at the microarchitectural level and to synthesize attacks exploiting these susceptibilities. In particular, I am analyzing virtual memory-specific aspects of a microarchitectural model to study exploits on other storage structures besides the cache, such as the translation lookaside buffer (TLB).

This work is part of the Check Tool Suite.