seL4: the journey of a verified kernel deployed in real systems
Abstract
With formal proofs of its correctness and security, seL4 provides the strongest assurance and isolation between untrusted and trusted components running in critical software systems, demonstrably preventing cyber attacks from endangering critical functionality and from propagating further. seL4 is being adopted in a number of sectors, from automotive to IoT, Defense, and more. The open-source seL4 Foundation provides the underlying support for its growing ecosystem of developers, contributors and adopters, and Proofcraft keeps pushing the roadmap of seL4's verification to make its formal proofs apply to more platforms, more features, and more properties. The talk will give an overview of seL4's journey and roadmap ahead.
Speaker Bio
June Andronick is CEO and co-founder of Proofcraft, a company providing commercial support for software verification in general and the seL4 microkernel verification in particular. She is also CEO of the seL4 Foundation, supporting the technology and community of seL4 users, adopters and developers. June has extensive leadership experience towards making the vision of verified software a reality in mainstream critical software. She was previously leading the Trustworthy Systems group, and contributed to the original seL4 verification. She holds a PhD in Computer Science from the University of Paris-Sud, France.