BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Neutrality and The Atoll Verified Hypervisor - David Cock
DTSTART:20260417T130000Z
DTEND:20260417T140000Z
UID:TALK246019@talks.cam.ac.uk
DESCRIPTION:Designed for organisations that cannot compromise on trust\, N
 eutrality is building Atoll\, a formally-verified\, secure\, European-sove
 reign virtualisation and cloud hosting platform. Atoll provides a mathemat
 ical proof of isolation between customer workloads\, delivering a new leve
 l of assurance. Atoll builds on the foundation provided by the formally-ve
 rified seL4 microkernel\, extending its formal correctness proof and platf
 orm support to securely run colocated commercial workloads handling sensit
 ive data on commodity hardware. \n\nIn this talk I will introduce both Neu
 trality\, a Swiss start-up applying formal verification to Systems code an
 d Atoll\, the platform we are building. Atoll will provide the isolation g
 uarantees of the seL4 Integrity theorem lifted to the level of isolation b
 etween colocated virtual machines handling sensitive or regulation-restric
 ted data. I will give an overview of the design and emphasis both on engin
 eering aspects as well as how we are designing for long-term\, maintainabl
 e verification.\n\nNeutrality will be growing over the next few years\, an
 d has recently been successful in raising blended funding through the EIC 
 Accelerator Grant. I will outline our current hiring plans and give an ove
 rview of the opportunities likely to be available to both Systems and Veri
 fication candidates in the short to medium term.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR