There is now a YouTube channel run by the seL4 Foundation. It presently has two playlists, one with the recordings of the seL4 material from this year’s UNSW Advanced Operating Systems course, and one with seL4 Summit talks from Trustworthy Systems.
More to come, enjoy.
Announcing the releases of seL4, CAmkES and CapDL under the seL4 Foundation. Below you can find links to release notes with updates to other supporting projects to come before the end of the year. Versioned Releases:
- seL4 12.0.0 ~ https://docs.sel4.systems/releases/sel4/12.0.0
- CAmkES 3.9.0 ~ https://docs.sel4.systems/releases/camkes/camkes-3.9.0
- CapDL 0.2.0 ~ https://docs.sel4.systems/releases/capdl/0.2.0
The 3rd seL4 Summit will take place (virtually) on 15–18 November (US East Coast time). The program features a tutorial and 3 days packed with great talks and panels.
Presentations will be streamed according to the schedule and available for download right after, and there will be an on-line discussion forum.
Registration is only $80US
We’re happy to announce the newest member of the seL4 Foundation: Minneapolis-based company Adventium Labs. Adventium Labs develops solutions for safe and secure software-intensive complex systems, with specialties in separation architectures, model-based system engineering, and mathematical analysis technologies. They are leveraging these capabilities to extend seL4 into safety and security critical industries, including medical devices, defense and commercial avionics, and industrial control.
RISC-V (RV64) is the third ISA with verified seL4. The functional correctness proof of seL4 on the RV64 ISA has completed. Congratulations to the awesome Proof Engineering Team of the Trustworthy Systems group on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible.
What we have now is the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future.
More on this in this blog post.
Yet another contribution of [UNSW Sydney](https://www.unsw.edu.au) to the seL4
community: This year Gernot Heiser is making the seL4-related videos from his
UNSW Advanced Operating Systems class freely available. You'll find them at the
[UNSW CSeLearning COMP9242 YouTube
channel](https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV).
At present there are the first two modules, which provide some background on
microkernels and seL4, and discuss the seL4 API. More material will show up over
the next two months.
The complete course material, including all lecture slides, the project spec and
code, are available, as always, from the [COMP9042 web
site](https://www.cse.unsw.edu.au/~cs9242/current/).
The whitepaper "The seL4 Microkernel - An Introduction" provides an
introduction to and overview of seL4. We explain what seL4 is (and
is not) and explore its defining features. We explain what makes
seL4 uniquely qualified as the operating-system kernel of choice
for security- and safety- critical systems, and generally embedded
and cyber-physical systems. In particular, we explain seL4's
assurance story, its security- and safety-relevant features, and
its benchmark-setting performance. We also discuss typical usage
scenarios, including incremental cyber retrofit of legacy systems.
You can download here.
We’re happy to announce the first new member since the launch of the seL4 Foundation: Sydney-based company Breakaway Consulting. Through Founder and Managing Director Ben Leslie, Breakaway comes with 20 years of experience in L4 microkernels and systems based on various L4 kernels. Prior to founding Breakaway, Ben was a student with what is now the TS Group, and then VP Engineering of Open Kernel Labs. Breakaway offers consulting services on architecture, design and implementation of seL4-based systems.
The Trustworthy Systems group is excited to announce the creation of the seL4 Foundation. Its aim is to provide a neutral and independent organisation to ensure the longevity of seL4, and grow its ecosystem of adopters and contributors. It has a high-profile Board consisting of Gernot Heiser (Chair), June Andronick, Gerwin Klein, John Launchbury, Sascha Kegreiß, Daniel Potts. It already has a number of members, including major adopters HENSOLDT Cyber and Ghost Systems, and providers of services for seL4, Cog Systems and DornerWorks. Please check the membership page for details and how to join. The seL4 Foundation is set up under the Linux Foundation, which provides a mature and well-known framework.
More information on the Blog post about "The seL4 Foundation — What and Why", and in the press releases from the Linux Foundation.