seL4 celebrated three key anniversaries in 2024. To celebrate these key anniversaries, a special panel will gather at the seL4 Summit 2024 to reflect on the journey over the past 20 years and discuss the future ahead.
The panel will cover the journey from the early days (2004-2009) to the developments over the years (2009-present), and then look to the future, with key players outlining their visions for seL4 in the next 20 years. The panel will be a mix of in-person anecdotes, videos, and quotes, including participants from Collins Aerospace, DARPA, Dornerworks, Kry10, Proofcraft, The University of Melbourne and UNSW.
The panel will be moderated by Nick Spinale from Colias Group, LLC.
The seL4 Foundation thanks NIO for becoming a Silver sponsor of the seL4 Summit 2024.
NIO is a global EV company funded in 2015 and that went public in the U.S. in 2018. NIO emphasizes user experience and technology innovation. NIO is a strong supporter of seL4 and a premium member of the seL4 Foundation. It has been investing heavily on building a full-fledge software platform for modern vehicles based on seL4.
The seL4 Foundation is pleased to welcome Lewis & Clark College as our latest member.
Lewis & Clark is a private, liberal arts college located in the Pacific Northwest of the United States. In our mathematical sciences department, we are pursuing the goal of making single-function connected devices more secure. Towards this end, we are proving a minimal, pure IPv6 networking stack implementation correct. We rely on seL4's infrastructure (i.e., microkernel, microkit, and device driver framework) as well as seL4's methodologies (e.g., proofs verified by Isabelle/HOL).
The seL4 Foundation thanks Kry10 for becoming a Gold sponsor of the seL4 Summit 2024.
Kry10 offers a full-featured operating system on top of the seL4 kernel, along with tooling, services, key management and more. The Kry10 Platform is a fast and easy way to build highly secure, next-generation cyber-physical devices. It leverages the verification of seL4 to provide a secure, self-healing, truly dynamic system with minimal downtime, even during upgrades.
Kry10 is an Endorsed Service Provider of the seL4 Foundation, offering support to enable seL4-based secure projects to be affordable, maintainable, and remotely manageable.
See here if you are interested in sponsoring the seL4 summit 2024.
The seL4 Foundation thanks Collins Aerospace for becoming a Bronze sponsor of the seL4 Summit 2024.
Collins Aerospace, part of seL4 Foundation member Raytheon Technologies, has been a long-time core participant in the seL4 ecosystem. It was a prime contractor in the DARPA HACMS program, which demonstrated the seL4-based incremental cyber retrofit of autonomous military vehicles. This was a major milestone in the growth of seL4, demonstrating that it protects against cyber attacks on real systems in operation. The same team also led the follow-on DARPA CASE program, aiming at designed-in cyber-resiliency, including the seL4-based framework for verified initialisation and configuration of systems architectures.
Collins Aerospace is now leading the INSPECTA team as part of DARPA's PROVERS program, which aims at developing formal methods tools to guide software engineers through designing proof-friendly software systems and reduce the proof repair workload.
See here if you are interested in sponsoring the seL4 summit 2024.
The seL4 Foundation thanks TII for becoming a Bronze sponsor of the seL4 Summit 2024.
The Technology Innovation Institute’s (TII) Secure Systems Research Centre (SSRC) aims to drive end-to-end security and resilience in cyber-physical and autonomous systems that will ensure safety. The research center adopts an applied research approach, emphasizing practical applications. By employing seL4 as both a microkernel and a hypervisor, SSRC seamlessly aligns its dedication to security with the foundational technology crucial to achieving its objectives. This critical technology forms the cornerstone of secure software stacks for diverse edge devices, including secure communicators and drones. TII’s research not only contributes to but propels the evolution of cutting-edge high-end edge device environments. TII’s SSRC focus centers on resilience, isolation, trust, and security, all with the intention of fostering a more secure digital landscape.
See here if you are interested in sponsoring the seL4 summit 2024.
This year marks a very special seL4 day anniversary.
20 years ago, the L4.verified project started, with the ambitious aim to formally verify an entire microkernel of the L4 family. seL4 was born.
15 years ago, on the 29th of July 2009, the original functional correctness proof of seL4 was completed, a widely-recognised research breakthrough and the first big milestone in seL4's history.
10 years ago, on the 29th of July 2014, seL4 was open-sourced, an instrumental step towards its adoption in a number of sectors.
To celebrate these key anniversaries, a special panel will gather at the seL4 summit 2024 to reflect on the journey over the past 20 years and discuss the future ahead. Stay tuned for more info.
It’s been a long time coming – we’re pleased to announce the release of
- seL4 13.0.0: The seL4 microkernel
- Microkit 1.3.0: The seL4 Microkit for building static-architecture systems
- CAmkES 3.11.0: Component Architecture for microkernel-based Embedded Systems
- capDL 0.3.0: Tools for generating, parsing and loading capability distribution specifications
- rust-sel4 1.0.0: Rust support for seL4 userspace. See seL4/rust-sel4 on GitHub for more information.
Microkit 1.3.0 and rust-sel4-1.0.0 are the first official releases under the seL4 foundation.
Enjoy!
Have a look at the program of the seL4 summit 2024. We have a great line-up of interesting seL4 work, with a combination of technical research and development, experience reports of seL4 in the field, technical discussions and birds-of-a-feather sessions.
Program at a glance. Go to the full program.
We are pleased to announce that the two keynotes for the seL4 summit 2024 will be Darren Cofer from Collins Aerospace and Ning Qu from NIO. Darren will talk about Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA) and Ning about seL4 in Software-Defined Vehicles: Vision, Roadmap, and Impact at NIO.
Darren Cofer is a Principal Fellow at Collins Aerospace. He
earned his PhD in Electrical and Computer Engineering from The University of
Texas at Austin. His area of expertise is developing and applying advanced
analysis methods and tools for verification and certification of
high-integrity systems. His background includes work with formal methods for
system and software analysis, the design of real-time embedded systems for
safety-critical applications, and the development of nuclear propulsion
systems in the U.S. Navy. Dr. Cofer has served as principal investigator on
many government-sponsored research programs, developing and using formal
methods for verification of safety and security properties. He served on
RTCA committee SC-205 developing new certification guidance for airborne
software (DO-178C) and was one of the developers of the Formal Methods
Supplement (DO-333). He is currently a member of SAE committee G-34
developing certification guidance for the use of machine learning
technologies onboard aircraft.
Ning Qu is a veteran in the autonomous driving industry and
a seasoned technical leader with extensive experience in operating systems,
high-performance runtime frameworks, and hardware-software co-design.
Currently, Ning serves as the Senior Director of the SkyOS team at NIO,
where he spearheads the development of SkyOS—a comprehensive suite of
platform software (including hypervisor, operating systems, and middleware)
for Software Defined Vehicles, showcased at NIO IN 2023. Before joining NIO,
Ning managed Waymo's ML Runtime team, playing a pivotal role in SF
Rider-only driverless launch on the Jaguar EV. At Baidu, he built the Apollo
OS from the ground up, establishing the foundation for the Apollo project.
Notably, he architected and developed Cyber RT and led Baidu's fully
driverless launch in 2020. Ning holds a B.S. and Ph.D. from Peking
University and has served as a researcher at CMU.
The seL4 Foundation thanks UNSW Sydney for becoming a Bronze sponsor of the seL4 Summit 2024.
seL4 was created by the Trustworthy Systems (TS) team, which is now part of the UNSW, a founding member of the seL4 Foundation.
The team has a track record of designing and implementing systems software for performance and reliability, and using rigorous formal methods to prove that they meet their security and reliability goals. Their aims are to:
- shift the software industry away from ad-hoc, unreliable engineering practices, and towards more principled and trustworthy methods; and
- make verified software a default choice, especially in safety- and security-critical systems.
The team works with government and commercial partners, as well as the broader software engineering community, to drive this change.
The seL4 Summit 2024 will take place in Sydney, the hometown of Trustworthy Systems and UNSW.
See here if you are interested in sponsoring the seL4 summit 2024.
The seL4 Foundation thanks Proofcraft for becoming a Bronze sponsor of the seL4 Summit 2024.
Founded by the seL4 verification leaders, Proofcraft offers commercial support, verification projects, training and consulting on formal verification in general, and involving seL4 specifically. By applying mathematical machine-checked software verification, Proofcraft increases critical software systems' reliability, safety and security, for a verified future.
The seL4 Summit 2024 will take place in Sydney, the hometown of Proofcraft.
See here if you are interested in sponsoring the seL4 summit 2024.
The seL4 summit 2024 will be held in Sydney, Australia, 15-17 October 2024.
The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people.
Tickets include:
- Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions
- Networking with other seL4 experts and enthusiasts
- Reception and dinner
The early bird cut-off date is 15 September 2024.
Local seL4 Sydney-siders will look into organising some informal activities for Monday 14 October 2024, before the summit kicks off, for anyone who wants to join. Gernot may also organise a bush walk for the weekend before the summit. Stayed tuned for more info!
The seL4 Foundation is pleased to welcome Apple as our latest member.
We are excited to see their interest in seL4 and look forward to seeing their work with seL4.
We are extremely pleased to announce that the functional correctness proof for seL4 on the 64-bit Arm architecture (AArch64) is complete!
We congratulate to our member Proofcraft for this great achievement, which marks a major milestone in the development of the seL4 microkernel and its ecosystem.
We also would like to express our immense gratitude to UK’s National Cyber Security Centre (NCSC) for funding this work, which is of great importance for the seL4 ecosystem.
For more information check Proofcraft’s news item.
Call For Presentations for the seL4 Summit 2024
- Share your seL4 work
- Share your seL4 experience
- Share your seL4 thoughts
Check the full Call For Presentations. To propose a talk, upload an abstract of one page or less by 22 April 2024 to the submission portal.
Also note the open invitation for a 5-minute slot to talk about your seL4 deployment.
We are thrilled to announce our program committee for the seL4 Summit 2024. Our awesome team comes from various parts of the seL4 ecosystem: users, contributors, committers, experts, advocates, researchers, and engineers.
It is our pleasure to confirm that the seL4 Summit 2024 will be in:
Sydney, Australia, 15-17 Oct 2024.
We look forward to welcoming the community in the birthplace of seL4.
We will announce a Call for Presentations in the coming weeks. Stay tuned!
