Announcing the seL4 Foundation

2019-10-21 With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing, and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims.

Qian Ge and co-authors win Best Paper award at EuroSys 2019

2019-10-10 The paper "Time Protection: The Missing OS Concept” by Qian Ge, Yuval Yarom, Tom Chothia (U Birmingham) and Gernot Heiser won Best Paper at the Tier-1 EuroSys conference in Dresden, Germany. It presents the first principled approach to preventing information leakage by timing channels, a problem the research community had ignored until it was highlighted by the Spectre exploit a year ago. The paper defines the new concept of time protection, shows how it can be implemented in the high-assurance seL4 microkernel, and demonstrates that it is highly effective in eliminating information leakage to the degree that hardware provides the right mechanisms. The results also confirm the team’s earlier claims that true information security will need a new hardware-software contract. You can see more here. Congrats to the team!

Congratulations to Dr Qian Ge!

2019-10-04 Congratualtions to Dr Qian Ge, who has just been awarded her PhD! Qian had been working on inventing highly optimised OS mechanisms for mitigating microarchitectural timing channels which obtain data leakage through resource contention. Her and her co-authors proposed a new system concept, time protection, as an OS abstraction, which offers mandatory temporal isolation analogous to the spatial isolation provided by the established memory protection abstraction. Time protection provides security guarantees against microarchitectural timing channels through a combination of temporal and spatial isolation techniques. Using our prototype in the seL4 microkernel, they demonstrated that time protection is both lightweight and effective.

Congratulations to Dr Liam O'Conner!
2019-09-26 Congratulations to Liam O'Conner, who has just been awarded his PhD! Liam has been instrumental in the design of the Cogent language, a functional systems language that can be reasoned about, while producing fast C code. A major part of his thesis was formalising the refinement from a functional semantics to an imperative semantics of Cogent by using linear types.

June Andronick is an invited speaker to FM'19
2019-06-06 FM '19 is the third world congress on Formal Methods (held every 10 years). It's is in Porto this October, where our research group leader June Andronick is an invited speaker! You can learn more about FM'19 from this video.