Program
| Sunday, June 16, 2019 |
|---|
| 09:00 - 10:00 |
Keynote: Peter Sewell
Nailing Down the Architectural Abstraction |
| 10:00 - 10:30 |
Coffee break |
| 10:30 - 11:30 |
Keynote: Gernot Heiser
Time protection: principled prevention of timing channels (slides) |
| 11:30 - 12:00 |
Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez
Short paper: Principled Detection of Speculative Information Flows (paper) (slides) |
| 12:00 - 12:30 |
Short Presentations:
Thomas Bauereiss
Formally Proving Security Properties of CHERI Architectures (slides)
Roberto Guanciale
Confidentiality-Preserving Refinement (slides)
Hira Syeda
Reasoning about ARMv7-style Translation Lookaside Buffers (TLBs) |
| 12:30 - 14:00 |
Lunch break |
| 14:00 - 15:00 |
Keynote: Frank Piessens
Proving the security of interrupt handling against interrupt-based side-channel attacks: a case study (slides) |
| 15:00 - 15:15 |
Andreas Lindner, Hamed Nemati, Pablo Buiras, Roberto Guanciale, Swen Jacobs
Validation of Abstract Side-channel Models for Computer Architectures (paper) (slides) |
| 15:15 - 15:30 |
Florian Vanhems, Narjes Jomaa, Samuel Hym, David Nowak
On the Proof-Oriented Design of a Context-Switching Service in the Pip Protokernel (paper) (slides) |
| 15:30 - 16:00 |
Coffee break |
| 16:00 - 17:00 |
Keynote: Dominique Bolignano
Formal Proof of a Secure OS Full Trusted Computing Base (slides) |
| 17:00 - 17:30 |
Short Presentations:
Olivier Delande
Generating Bare-metal C Code from a High-level Pure Specification (slides)
Akram El-Korashy
A Fully-Abstract Translation of Pointers to Capabilities (slides)
Stéphane Lescuyer
Smart & ProvenTools: Proof Techniques that Scale (slides) |
|
