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