BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Roberto Guanciale (KTH) DTSTART:20210728T140000Z DTEND:20210728T150000Z DTSTAMP:20260423T021341Z UID:UK-SPS/5 DESCRIPTION:Title: I nSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis\nby Roberto Guanciale (KTH) as part of UK Security and Priva cy Seminar Series\n\n\nAbstract\nThe Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining\, out-of-order and speculation to extract ar bitrary information about the memory contents of a process. A comprehensiv e formal microarchitectural model capable of representing the forms of out -of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a mod el would be very useful\, as it would allow the existence and non-existenc e of vulnerabilities\, and soundness of countermeasures to be formally est ablished. We present such a model targeting single core processors. The mo del is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that und erpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities\, as well as to formally ana lyze the effectiveness of proposed countermeasures. Specifically\,we disco ver three new (potential) vulnerabilities\, including a new variant of Spe ctre v4\, a vulnerability on speculative fetching\, and a vulnerability on out-of-order execution\, and analyze the effectiveness of existing counte rmeasures including constant time and serializing instructions.\n LOCATION:https://researchseminars.org/talk/UK-SPS/5/ END:VEVENT END:VCALENDAR