Abstract

Designed for organisations that cannot compromise on trust, Neutrality is building Atoll, a formally-verified, secure, European-sovereign virtualisation and cloud hosting platform. Atoll provides a mathematical proof of isolation between customer workloads, delivering a new level of assurance. Atoll builds on the foundation provided by the formally-verified seL4 microkernel, extending its formal correctness proof and platform support to securely run colocated commercial workloads handling sensitive data on commodity hardware.

In this talk I will introduce both Neutrality, a Swiss start-up applying formal verification to Systems code and Atoll, the platform we are building. Atoll will provide the isolation guarantees of the seL4 Integrity theorem lifted to the level of isolation between colocated virtual machines handling sensitive or regulation-restricted data. I will give an overview of the design and emphasis both on engineering aspects as well as how we are designing for long-term, maintainable verification.

Neutrality will be growing over the next few years, and has recently been successful in raising blended funding through the EIC Accelerator Grant. I will outline our current hiring plans and give an overview of the opportunities likely to be available to both Systems and Verification candidates in the short to medium term.