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