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_.
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"
@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
