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 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.
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.
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.