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