Events and news relevant to the Laboratory for Foundations of Computer Science

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

We'll have an LFCS seminar next week:

  Tuesday, 26 May, 4.10pm
  Dominic Mulligan, Amazon Web Services, Cambridge

  This seminar is hybrid.

  Venue: IF G.03

  To attend remotely:
  URL: https://tinyurl.com/bdhzavhe

  (This is the first time I'm trying to run a hybrid LFCS seminar with Teams,
 I apologise in advance that this may not work.)

Dom is visiting us on the Tuesday only, please get in touch with him or me
if you want to meet, and please let me know if you'd like to come for dinner.


We're synchronising the seminar time with the teaching timetable, and
plan to start the talk at the advertised time, so please arrive a minute or 
two
earlier.


In detail:

----------------------------------------------------------------------
Dominic Mulligan, Amazon Web Services, Cambridge
https://dominicpm.github.io/

  Tue, 26 May, 4.10pm
  Venue: IF G.03
  Remote participation:
  URL: https://tinyurl.com/bdhzavhe



Title: Nitro Isolation Engine: formally verifying a production hypervisor

Abstract

Cloud computing relies on hypervisors to enforce isolation between
co-tenanted virtual machines. Hypervisors are therefore critical
security infrastructure, and assurance of their correctness is
paramount. Traditional engineering techniques—code review,
testing, fuzzing—provide strong assurance but cannot exhaustively
verify that isolation holds across all possible execution paths.
Formal verification extends and complements these approaches by
establishing mathematical guarantees about system behaviour.


This talk presents our experience applying interactive theorem
proving to verify a production hypervisor component: the Nitro
Isolation Engine. This is a trusted, minimalist computing base
written in Rust, enforcing isolation between virtual machines on AWS
Graviton5 EC2 instances. Designed for verification from inception,
we have specified the intended behaviour of this component and
verified correctness in the Isabelle/HOL interactive theorem
prover, producing approximately 260,000 lines of machine-checked
models and proofs.


Our verification establishes three key classes of property:


- Functional correctness: The system behaves as specified for all
operations including virtual machine creation, memory mapping, and
abort handling. Our total verification approach additionally
establishes memory-safety, termination, and absence of runtime
errors.


- Confidentiality: A noninterference-style property demonstrates
that guest virtual machine state remains hidden from an expansive
definition of observer monitoring system actions, formalised as
indistinguishability preservation up to permitted
declassification flows.


- Integrity: Guest virtual machine private state is unaffected by
operations on distinct virtual machines.


The talk will discuss the verification approach, key proof
techniques, and challenges in applying formal methods to production
systems.


----------------------------------------------------------------------

Upcoming seminars:
------------------
16 Jun: Shing Hin Ho, Imperial College London



If you would like to propose a speaker, or speak yourself, please contact me.
The seminar webpages:
http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,
Ohad.
The University of Edinburgh is a charitable body, registered in Scotland, 
with registration number SC005336. Is e buidheann carthannais a th’ ann an 
Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.