Loading Seminars

« All Seminars

  • This seminar has passed.

InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis

28 July 2021 @ 3:00 pm - 4:00 pm

The Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive 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 model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. We present such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically,we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of existing countermeasures including constant time and serializing instructions.

Zoom meeting: https://newcastleuniversity.zoom.us/j/81925495891?pwd=OGJkRnNWOEEwaXVkNUJUdUNTem9oQT09
Meeting ID: 819 2549 5891
Passcode: 495287

Youtube live stream: https://youtu.be/Gl9eJ-33duI

Youtube VoD


28 July 2021
3:00 pm - 4:00 pm
Seminar Tags:


Roberto Guanciale (KTH)

Roberto Guanciale is an associate professor within the Department of Theoretical Computer Science, EECS, KTH since 2015, where he works on system security and formal verification. He received his bachelor’s degree in Computer Science from University of Pisa in 2003, his Master from University of Pisa in 2005, and his Ph.D. from IMT Lucca in 2009. He has been a postdoctoral researcher at KTH (2012 - 2015). His research focuses on Computer Security, in particular on formal verification low level code and design of separation kernels. He also designed methods to analyze coordination of distributed services.

Leave a Reply

Your email address will not be published. Required fields are marked *