Do you (reading this) ever encounter situations where people use Sel4 "in the wild"? Like any practical purpose will do, as long as it isn't a poc/test
0 Boosts
0 Likes
This federated comment is not yet available here.
The L4 "microkernel family" (as some have described it) dates back to 1993? seL4, 2014 I guess? Fuschia supposedly began development circa 2016 (with initial public showings closer to 2021 I guess?)? So presumably Fuschia developers had prior art to think about as influential (or not) as that may be.
More recent realms in microkernel research have given us the CHERiOT RTOS (e.g. https://cheriot.org/book/core_rtos.html) and sigh I failed to book mark an ActivityPub thread earlier this year where some folks made mention of some other microkernels that were novel to me, and I want to dig into more deeply and trying to search for those again has been, not going so well. 😜 (if others see this and want to chime in where my searches and failures led and save me some grief, please do!)
L4, originally at least, was, as most microkernels are: tiny and could sometimes fit within the L1 cache of a CPU! Pretty impressive!
Apple uses L4 within their Secure Enclave supposedly? (Apple's Secure Enclave, last I looked, predated the existence of seL4)
seL4, specifically seems really into formal proof methodologies; yet having encountered similarly hyped systems, decades earlier, which used such methodologies claiming they were secure, only to also find exploitable bugs within such systems? I don't really regard such formalities very highly personally. Maybe from a scholastic rigor sense, they are useful for certain properties and drawing lines in the sand about some things being in or out "of scope"? Maybe if I had a PhD or something, it would be more intelligible to me instead of feeling as if such framings are often academic snake oil.
CC: @whitequark@treehouse.systems @mcc@mastodon.social @puppygirlhornypost2@transfem.social
@teajaygrey @tris @mcc @puppygirlhornypost2 seL4 is much older than 2014. but also it doesn't seem like you're interested in any productive discussion here, you're just dismissing something you haven't even bothered to look at. this is noise.
Sincerely not trying to dismiss anything, though you are correct. I misread a Wikipedia page and focused on 2014 instead of 2009?
https://en.wikipedia.org/wiki/SeL4#History
Maybe it is older than that? I do not know.
Writing off my interest in microkernels (beyond the L4 family) as "just noise" well, it's not going to stop my interest. My apologies if I somehow offended you unintentionally.
CC: @tris@chaos.social @mcc@mastodon.social @puppygirlhornypost2@transfem.social
@mcc Apple's Secure Enclave Processor OS is L4 based, though I'm not sure if the heritage is pure seL4, or a cherry-pick.
@mcc @joe The concepts are common in safety-critical systems such as automotive, though they tend to be the worst of closed proprietary systems. Formal proof itself is of limited use, because it's contextual—if you were to actually use this in e.g automotive, you'd need to assess it in the context of the whole system it resides in, toolchains, host build environment, and even developers themselves.
But the concept is (IMO) what all new OS should be based on. It's definitely an ongoing _thing_.
@mcc (Apologies... I'll answer the actual question better) The reduction in seL4 is to permit formal analysis. You can't do formal methods with anything larger than the tiniest of programs, and even seL4 is probably a stretch. I've been involved in a (proprietary) project which also required formal proof, and it has basically the same feature list.
But you don't need formal methods, outside of a few niche applications, and even then it's _contextual_ (as above). No need to specifically use "se"
I want to learn about how Sel4 works, but when I went to read the whitepaper it was very little about how it works and a great deal of "Sel4 is good, you should use it"
What I've learned about Sel4 from half a morning of reading things
1. What they seem to have made is a hypervisor with a pseudo-IPC mechanism which is really just a method for cooperatively picking which process gets to run next on the current core. This sounds fun and hilarious. I'm imagining Mac OS 7 but everything's a unikernel.
2. Everyone who's written software for SeL4 seems to be yelling NO NO GET AWAY like the Giant in the final episode of Twin Peaks S2
@mcc I am not especially familiar with hypervisors, but I have been trying to familiarize myself with seL4 and its attendant libraries. It does seem akin to hypervisors in that it primarily provides process separation and scheduling. In the MCS variant, which is the new version they seem to be building everything on, you can also bundle processes into "scheduling contexts" and attach or detach them from the scheduler.
What I'm really doing here is, I want to start trying to understand Redox (this is a long term project which I am attacking hilariously slowly, I'm still stuck on getting qemu to work right with Mutter), and I was thinking, hm, I don't know OS kernels well, I should probably read up on at least one other modern microkernel OS so I have a point of comparison. If SeL4 is "weird" or overfocused on formal-methods stuff, are there other going-concern/research kernels I should know? Does L4 yet live?
@mcc Funnily enough I was going to say Redox is likely the most useful "works today" reference for you to play with, but the caveat is it's a large project 😊 The main differentiator between the microkernel platforms is how *purist* they are. seL4 is very much towards pure, because they were forced to. Popular (practical) microkernels tends to be impure, with complex code technically not necessary in-kernel, for performance, but also because otherwise it increases the total *system* complexity.
SeL4 just casually dropping that they double as a hypervisor sounded really cool to me. "This microkernel is also a hypervisor" makes sense to me in some kind of galactic-logic aesthetic way. Is that an uncommon idea?
@soller Thanks!
Actually the thing I was looking at Sel4 for was I was curious if Sel4 software could be tricked into* running atop Redox, since as far as I know both all interesting kernel interactions are done via message passing, so maybe a kernel module could just translate messages.
I don't… I don't know why I wanted this. I think I was just curious if it was possible.
* Possibly recompiling it so the calls to send the "PPC" IPCs get converted into function calls to send "scheme" IPCs
@mcc As far as I know, Genode makes its userspace portable to different microkernels, but I'm not sure how that works at the low level. In principle, it may be possible, but there are lots of expectations that the Redox kernel has the Redox userspace
@soller @mcc https://youtu.be/N624i4X1UDw?is=iz-0Ojf3z9Kq7J2G could be inspiring.
Sculpt OS - A Dynamic General-Purpose OS Powered by Genode on seL4- Alexander Boettcher, Genode Labs
YouTube
@mcc@mastodon.social how do you even get into sel4
@puppygirlhornypost2 well, according to this whitepaper, you should get into it because its correctness has been formally verified
@puppygirlhornypost2 and if you think that answer is not responsive to your question, here's another five paragraphs about the formal verification process
@mcc yes (multiple times, but a long time ago)
@whitequark do you know if the people doing this are still using it? Or was the person you
One thing I'm trying to figure out is whether sel4 is a "going concern" that will be well supported on current hardware
@mcc it was a meeting at IARPA in 2014. i've kept up contact with one person since but he moved on to other (also quite good) things
@mcc one issue is that the Australian goverment org that was instrumental to its existence and success recently decided to defund the entire thing... but I think (I'm not plugged in enough) the project recovered from that by now
