POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 16:45 - 17:07 at Turing Lecture - Session 4 Chair(s): Dominique Devriese

NOVA is a microhypervisor that executes in a privileged kernel mode and that provides only basic services for virtualization, isolation, scheduling and management of physical system resources. NOVA’s design goal is to reduce the critical code base, and to leave richer virtualization features to user applications, such as a Virtual Machine Monitor (VMM), that run in a less privileged mode (e.g. user mode). The size (about 17K lines of code and 15 hypercalls) makes it a suitable target for formal verification.

In the talk, we present our on-going effort in formally verifying the concurrent NOVA microhypervisor in a modular, tractable approach. We show how to decompose the specifications and proofs of NOVA’s hypercalls using concurrent separation logic, and discuss the (open) challenges.

Sat 20 Jan

Displayed time zone: London change

16:00 - 17:30
Session 4PriSC at Turing Lecture
Chair(s): Dominique Devriese KU Leuven
16:00
22m
Talk
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC
Robert Künnemann CISPA Helmholtz Center for Information Security, Ethan Cecchetti University of Wisconsin-Madison
File Attached
16:22
22m
Talk
Gradual Verification for Smart Contracts
PriSC
Haojia Sun Shanghai Jiao Tong University, Kunal Singh Carnegie Mellon University, Jan-Paul Ramos-Davila Cornell University, Jonathan Aldrich Carnegie Mellon University, Jenna DiVincenzo (Wise) Purdue University
File Attached
16:45
22m
Talk
Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
PriSC
Hoang-Hai Dang BedRock Systems, David Swasey BedRock Systems, Gregory Malecha BedRock Systems
File Attached
17:07
8m
Day closing
Closing Remarks
PriSC
Shweta Shinde ETH Zurich