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.

Advisors: 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