Cameron Rasmussen
EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2019-95
May 24, 2019
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2019/EECS-2019-95.pdf
Spectre and Meltdown represented a family of new vulnerabilities called transient execution attacks. They have shown that micro-architectural state was taken for granted and side channels were capable of exposing more than was previously believed possible. This thesis addresses the problem of determining whether a given program is vulnerable to transient execution attacks. Using an approach based on formal methods, we formalize a secure speculation property, adversary and platform models, and use the UCLID5 tool to verify whether a given program satisfies the secure speculation property.
Advisor: Sanjit A. Seshia
BibTeX citation:
@mastersthesis{Rasmussen:EECS-2019-95, Author = {Rasmussen, Cameron}, Title = {Secure Speculation: From Vulnerability to Assurances with UCLID5}, School = {EECS Department, University of California, Berkeley}, Year = {2019}, Month = {May}, URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2019/EECS-2019-95.html}, Number = {UCB/EECS-2019-95}, Abstract = {Spectre and Meltdown represented a family of new vulnerabilities called transient execution attacks. They have shown that micro-architectural state was taken for granted and side channels were capable of exposing more than was previously believed possible. This thesis addresses the problem of determining whether a given program is vulnerable to transient execution attacks. Using an approach based on formal methods, we formalize a secure speculation property, adversary and platform models, and use the UCLID5 tool to verify whether a given program satisfies the secure speculation property.} }
EndNote citation:
%0 Thesis %A Rasmussen, Cameron %T Secure Speculation: From Vulnerability to Assurances with UCLID5 %I EECS Department, University of California, Berkeley %D 2019 %8 May 24 %@ UCB/EECS-2019-95 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2019/EECS-2019-95.html %F Rasmussen:EECS-2019-95