- Devel - lists.sel4.systems

RFC-28: remove support for IA-32
by Gerwin Klein 04 Nov '26

04 Nov '26

As previously discussed on this list and at the summit, here now the more detailed Request for Comments on removing support for IA-32 in seL4 https://github.com/seL4/rfcs/pull/44 Since there has only been confirmation that nobody is using seL4 on IA-32, I would even propose to already remove support in the next release without a longer deprecation phase. If there are any concerns, please do comment on the RFC. Cheers, Gerwin

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 30 Oct '26

30 Oct '26

We’re pleased to announce the release of - seL4 17.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/17.0.0 - Microkit 2.4.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/2.4.0 - CAmkES 3.13.1: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.13.0 - capDL 0.6.1: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.6.1 - rust-sel4 6.0.0: Rust support for seL4 userspace. See the Rust section on the seL4 docsite for more information. https://github.com/seL4/rust-sel4/releases/tag/v5.0.0 This release focussed on fixing issues in unverified configurations of seL4, as well as auditing code in verified configurations that is not covered by the scope of seL4’s formal proofs. Like previous releases, this release contains security relevant changes and we recommend upgrading to the latest version of seL4. We would like to thank Anthropic for reporting a number of these issues and for the constructive, actionable and useful way they were communicated. Overall, this audit has strengthened the security of seL4 in all parts of the kernel that the formal proofs do not make guarantees about. seL4 17.0.0 and the corresponding Rust support have breaking changes and will require updates if you are using the seL4 API directly. The CAmkES and capDL tool releases are backwards compatible. The Microkit contains security and bug fixes and has breaking changes. As always, a more detailed list of the changes and user-visible impact can be found in the seL4 release notes [https://docs.sel4.systems/releases/sel4/17.0.0] and the seL4 docsite [https://docs.sel4.systems/] together with upgrade instructions. Enjoy! Gerwin

1 0

seL4 developer hangout reminder
by Birgit Brecknell 26 Oct '26

26 Oct '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. - Tue 27 Oct, 21:00 UTC For your local date and time please see https://sel4.systems /stay-informed.html#calendar Note: seL4 Developer Hangout now uses Jitsi To start the meeting, please login (e.g. using google or github credentials). Once the meeting has started, anyone with the link can join. Jitsi link: https://meet.jit.si/seL4DeveloperHangout -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

Clarification on statement in manual of reuse of ASIDs
by Ben McCart 22 Oct '26

22 Oct '26

All, I am seeking some clarification from something in the manual (v12.0.0 - 16.0.0) regarding ASID assignment. The section in question is 8.3.1.6 'TLB invalidation'. The statement in part is "invalidating all mappings of an ASID (triggered by deleting a VSpace)". I was confused however as the section also contains ARM specific information and 8.3 is labelled as 'ARM-SPECIFIC I/O'. Can I depend on an ASID being unmapped when its associated vspace object is deleted on all supported platforms, or just on ARM? Is there something else I need to do to reuse ASIDs other than just delete the vspace object? Sincerely, Ben McCart

2 1

seL4 hangout cancelled for Wed 14 Oct
by Birgit Brecknell 14 Oct '26

14 Oct '26

Hi all Unfortunately we've had to cancel the seL4 hangout today. It will be on again in a fortnight. Sorry for the late message. cheers Birg -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

seL4 developer hangout reminder
by Birgit Brecknell 12 Oct '26

12 Oct '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. - Wed 14 Oct, 7:00 UTC For your local date and time please see https://sel4.systems /stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

question about GICC interface failure with microkit VM
by Christian Bruel 08 Oct '26

08 Oct '26

Hello, I am trying to migrate a STM32MP2 Linux VM from the CAmkES VMM to the Microkit VMM. After filling the few platform definitions in vgic.h and vmm.h, I can boot the Linux VM up to the point where it faults during gic_init in linux: vmm|ERROR: unexpected memory fault on address: 0x4ac20004 This address happens to maps the GICC interface The Microkit VMM qemu example in the tutorial I used as a starting point only maps the GICV interface, so I tried adding the following region to the Microkit xml port description: <memory_region name="gic_cpu" size="0x2000" phys_addr="0x4ac20000" /> which cause the Microkit trace failure: ERROR: object 'frame_mr_gic_cpu_000000000', with paddr 0x00004ac20000..0x00004ac21000 is not in any valid memory region. Below are the valid ranges of memory to be allocated from: Valid ranges outside of main memory: [0x000000000000..0x000040000000) [0x000040000000..0x000048000000) [0x000048000000..0x00004a000000) [0x00004a000000..0x00004a800000) [0x00004a800000..0x00004ac00000) [0x00004ac00000..0x00004ac10000) [0x00004ac11000..0x00004ac12000) [0x00004ac12000..0x00004ac14000) [0x00004ac14000..0x00004ac18000) [0x00004ac18000..0x00004ac20000) [0x00004ac21000..0x00004ac22000) ... So there appears to be a hole exactly over 0x4ac20000..0x4ac21000, which is where the GICC registers live. Are these “valid ranges” derived directly from the kernel’s device resources to the root task? before checking the xml memory_region ? If so, what could cause the kernel to exclude exactly this page? Since this setup works with the CAmkES VMM, I would not expect a general device-tree parsing issue, Is there a way to trace valid device memory ranges construction in Microkit ? Thanks for any hints Best regards, Christian

2 2

Are there any users of 32bit seL4/x86 left?
by Gerwin Klein 05 Oct '26

05 Oct '26

Before I write up a proper RFC for this, a poll: Is anybody still using the 32-bit x86 support of seL4? Given that Microkit only supports x64 and even most Linux distributions have removed support for 32 bit x86, my impression is that this port is now mostly unused. Since it is a maintenance burden, it would make sense to phase out support for it in seL4 so there is more time available to concentrate on newer hardware. If you don’t want to reply publicly for some reason, it’s fine to email me privately. No matter the outcome, there will be an official RFC with the usual comment period before anything is decided. Cheers, Gerwin

2 1

Re: on using the GPL (was: Re: Announcing Neptune OS v0.4, now running Linux kernel drivers in userspace on seL4)
by Dr. Chang Liu, PhD. 24 Sep '26

24 Sep '26

Hi Martin and Branden, Thank you both for the discussions. My main goal of picking the GPLv3 license is to ensure all changes to Neptune OS itself be made public, so a corporation wouldn't be piggy-backing on free software without giving back to the community. My goal is not to prevent one from running proprietary software or from shipping a commercial product based on Neptune OS, although I do understand that GPLv3 may have been perceived to prevent the former. In the VM scenario discussed above, our architecture means that this closed-source VM image is running in an isolated user process that communicates with the rest of the system only via the seL4 IPC, so it's running along side GPLv3 software, not as part of it (there is a small, dynamically linked shim library involved that constructs the messages for IPC, but that library is only for convenience. You can build the IPC messages yourself, or contact me to request this small library be dual-licensed). In any case, if you do plan to use Neptune OS in any project, commercial or otherwise, I'd love to hear from you to discuss any technical or legal issues you have concerns about. Best, Chang --- Dr. Chang Liu, PhD. github.com/cl91/NeptuneOS On Wed, Sep 23, 2026 at 10:30 AM G. Branden Robinson < g.branden.robinson(a)gmail.com> wrote: > Hi Martin, > > At 2026-09-23T02:15:23+0300, Martin Vahi via Devel wrote: > > On 2026_09_20 16:31, Dr. Chang Liu, PhD. via Devel wrote: > > >... > > > I am announcing release v0.4 of Neptune OS [0], a general purpose > > > Windows NT-like operating system built on top of seL4. > > >... > > > > Looks interesting, but the > > > > https://github.com/cl91/NeptuneOS/blob/master/LICENSE > > > > says GPL version 3 and does not mention that it is OK to link to > > operating system interface libraries without forcing the GPL version 3 > > on the userspace applications. The way I understand the GPL version 3, > > the GPL license is also infectious through dependence. For example, > > if someone creates a virtual appliance that runs the GPL version 3 > > based Neptune OS and that virtual appliance is used as a dependence to > > some business application that runs at that appliance as a userspace > > application, then the userspace application, the business application, > > is forced to have a GPL version 3 license, because it "forms a larger > > program"(phrase from GPLv3) with that virtual appliance. > > I think your understanding is dependent on several assumptions popularly > spread by opponents of copyleft in the tech sector, including by Apple > for the past 25 years or so, because Steve Jobs appears to have carried > a lifelong grudge against copyleft licensing. Jobs seems to have held > the Free Software Foundation in special antipathy, since we can infer > that the attorneys retained by NeXT Computer, Inc. advised their client > that the GCC front end for Objective-C that it developed (or acquired) > fell within the GPL's purview as a "Work based on the Program". (Given > the date, this license would have been what we retrospectively call > "GPLv1".[a]) > > Little around the technological details of how a "Work" comes to be > "based on" a GPL-licensed "Program" has been decided by courts. > Litigation involving the GPL is relatively rare, and to my knowledge > there hasn't been a case of criminal copyright infringement in its terms > brought anywhere in the world, ever--except in Germany.[b] What we did > come to learn, after many long years of almost total uncertainty, is > that (a) the GPL is not a toothless license; and (b) in the United > States, its terms are enforceable within the framework of contract law, > and not copyright alone.[c] > > From several perspectives, the total paucity of criminal copyright > enforcement of GPL violations by government prosecutors is a good thing. > But one consequence is that what litigation (or threat thereof) there > has been involving the GPL has been in the civil (or "tortious") > regime--in other words, courts of equity rather than "law" in common law > jurisdictions. And a consequence of _that_ is that the public, and even > major players in the contested space, like major tech firms shipping > GPL-licensed software, and not-for-profit organizations that advocate > for the GPL, like the Software Freedom Conservancy or the Free Software > Foundation, get little insight into what sorts of arguments prove > persuasive in negotiations between opposing litigants, as these cases > are almost invariably settled, and the terms of the settlements usually > confidential. > > This state of affairs contributes to a culture of folklore among > corporate counsels and creates opportunities for the spread of FUD > (fear, uncertainty, and doubt) in the software engineering community, > especially by those who expect a financial upside from discouraging > adoption of the GPL and enforcement of its terms. Germany offers a good > test of this hypothesis, and I wonder if any scholars of law or commerce > there have studied the question. > > Resistance to copyleft enables _enclosure_ of software systems. You may > be familiar with a criticism of Microsoft's anti-competitive practices > with respect to industry standards over many decades, which the firm > characterized as "embrace and extend". "And extinguish", concluded > skeptical observers. Enclosure of various digital commons has been a > standard business model for decades. Cory Doctorow has written notably > about this process.[d] > > Consider a "Program" in a compiled language like C or C++ that produces > a machine language object file (".o"). > > Here are some matters that are not "settled law", to my knowledge: > > * whether "static linking" creates a "Work based on the Program" > > (Engineers tend to think it does.) > > * whether "dynamic linking" creates a "Work based on the Program" > > (Engineers argue vigorously over that.) > > * whether dlopen(3)ing an ELF object can alter the answer to the > foregoing, and what that means for one's obligations under the GPL if > the dlopening of an ELF module is not exercised by the Program in its > shipping configuration, but only after reconfiguration by the end user > > * whether use of IPC mechanisms, mmap(2), or similar techniques changes > the answers to any of the foregoing > > The terms of the GPL indeed (in my reading) attempt to consider all of > the foregoing scenarios, in language broad enough to be intelligible to > legal professionals. I reiterate that my point is that these matters > have not been _tested in court_ to my knowledge. > > Now consider a "Program" that is an operating system kernel. > > Here's another element of unsettled law, to my knowledge: > > * whether a "software trap" or a "system call" creates a "Work based on > the (kernel) Program" > > (As you noted in passing reference to its exception clause, the Linux > kernel license explicitly rules this out.) > > Did the famous U.S. Supreme Court case _Google LLC v. Oracle America, > Inc._ (the Java/Dalvik case) resolve any questions about software > copyright? Yes and no. A popular view is that copyright generally does > not attach to "header file declarations" because (a) they are _designed_ > to achieve _interoperability_ with third-party works, and (b) in popular > programming languages, the space available for "original expression", a > statutorily essential element of copyright in the U.S., is minimal. > > In C, for example, practitioners generally believe that, having settled > on an API in the abstract (an "idea"), there is a "right way" to write > the ".h" files for it, and trying to establish a copyright in such a > file by larding it with "original expression" would serve only to > obfuscate its purpose, and/or make its processing inefficient. > > However, the Supreme Court did not reach this question, because it ruled > that Google's use of Oracle's (Sun Microsystems's successor-in-title) > Java APIs via the equivalent of "header files" constituted _fair use_, > an important carve-out to liability under copyright law.[e] > > > That is to say, if a freelancer like me wants to deliver the software > > that I self write as a service to my client(s), and I want to deliver > > a QEMU virtual appliance that has all the dependencies of my software > > included in it, then I can not use Neptune OS in that virtual > > appliance. I suggest that the license is changed so that it is clear > > to everybody that using Neptune OS as a wrapper or a dependence of > > software that runs as a Neptune OS userspace process does not infect > > the userspace process with GPL. If Neptune OS switched to LGPL or some > > Linux style GPL+exceptions, then that would be fine. Without the > > license change the Neptune OS will stay an academic curiosity that > > will NOT be adopted to real world use, unless the Neptune OS authors > > hope to sell the Neptune OS copyrights to some megacorporation and > > that megacorporation then changes the license. > > I offer two pieces of layperson's advice. > > 1. Retain the services of an attorney practicing in your jurisdiction > who is competent in the copyright laws applicable there. This > practice is almost basic due diligence for a software freelancer, in > my opinion. Set your consulting rates to offset the retainer that > your attorney charges and be frank with your clients that you are > doing this. Consider what your client implies about their > intentions if they want you to work so cheaply that you cannot > afford legal counsel. > > 2. I think Dr. Chang Liu, PhD., is better advised to maintain > NeptuneOS's public copyright exactly as it is. If you wish to > employ that work as part of a solution that you offer for sale to > your own clients, and do not wish to abide by the requirements of > the GNU GPL, then you can privately negotiate with Dr. Liu for > alternative terms. In other words, you can purchase (or agree upon) > a license from Dr. Liu just as you might from a traditional, > proprietary software vendor. > > I feel ethically bound to make some disclosures. > > A. I am not a lawyer, and this is not legal advice. > > B. I worked for several years in FLOSS software licensing compliance > for a "Fortune 50" company in the United States. This work included > regular (weekly) meetings with corporate counsel to discuss and > develop recommended best practices for engineering staff. > > C. I was once employed by Trustworthy Systems (in CSIRO/Data61 days). > > D. I perform volunteer engineering labor for the Free Software > Foundation. > > E. I served on "Committee A" of the GNU GPLv3 revision team circa 2006. > > > thank you for reading my letter. > > Thank you for your patience with mine, and for considering my response. > > Regards, > Branden > > [a] https://ebb.org/bkuhn/talks/LinuxTag-2011/compliance.html > [b] https://www.jipitec.eu/jipitec/article/view/41/37 > [c] > https://www.dglaw.com/breach-of-contract-claims-allowed-for-alleged-open-so… > > https://sfconservancy.org/news/2025/dec/04/tentative-vizio-ruling-in-favor-… > [d] https://www.versobooks.com/products/3341-enshittification > > I'm reminded that enclosure of the agricultural commons was > essential to creation of the nobility as we now know it in England > and Wales starting four hundred years ago. The very term > "wasteland" acquired the negative connotation it has today because > the lords and ladies of England regarded any acreage that was > productive neither of ground rents nor of profits from cash crops > to be "wasted" (albeit redeemable if used for fox hunting). > > [e] https://www.scotusblog.com/cases/google-llc-v-oracle-america-inc/ >

2 1

Cohesix 1.1.0-beta: Pi boot and edge GPU demos
by Lukas Bower 24 Sep '26

24 Sep '26

Hi All, Great to see the various project activities here. Inspired by other great projects, I’ve posted five short Cohesix 1.1.0-beta demos: 1. Pi 4 boot tour (2:40): SD image, U-Boot, HDMI and serial startup, and root shell commands. https://youtu.be/63kroQa_sys 2. Raw Pi 4 boot (1:17): the HDMI and serial output through one boot and shell sequence. https://youtu.be/Iarz2uBwnaY 3. CUDA workflow (1:07): CUDA is NVIDIA’s platform for running computation on a GPU. The Jetson does that work; the Pi and Mac provide control and inspection. This clip includes a live Jetson check and a SwarmUI example. https://youtu.be/cf0x8659WvI 4. Edge visual adapter (0:58): a short model-adaptation workflow using the Jetson and SwarmUI. https://youtu.be/lmCR_0Pnaac 5. Canary recovery (1:01): inspecting a failed trial and recovering safely in SwarmUI. https://youtu.be/OKvjddbSsFs Source and release notes: https://github.com/lukeb-aidev/cohesix I’d welcome feedback, particularly on the Pi boot path and capability boundaries. Best, Lukas

1 0