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 Proocraft'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!
