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)
Online user: 1