3 ms·

What kind of appliances have you created/planned? I love the idea of seL4, and was sorely disappointed to see Australia cut their funding. Decades of exploits

What kind of appliances have you created/planned? I love the idea of seL4, and was sorely disappointed to see Australia cut their funding. Decades of exploits have me convinced that microkernels are the only real path towards security.

als0 4y ago
> Decades of exploits have me convinced that microkernels are the only real path towards security. Not necessarily. Check out the CHERI project, which has a reasonably good handle on exploits https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
astrange 4y ago
Australia seems to have a lot of quality CS research (well, that, Mercury, and… WWJDIC), and no way to productize any of it.
im_down_w_otp 4y ago
We at one point created a specialty OS for some exotic network hardware designed for very fancy robots. For a brief period we were using seL4+Ferros like kind of a hypervisor used as the integration point for our "system-level" V&V tools based on what we learned making the aforementioned OS, but we abandoned that approach for non-seL4 reasons. We'll offer something of a "black box recorder" for robots and other cyber-physical systems that's also for runtime verification. Well, seL4 is now managed under a foundation as part of the Linux Foundation umbrella. The seL4 Foundation. Ultimately, I think it might be for the best. Now there are more seL4 researchers and practitioners out in industry working to integrate and build upon seL4 as a building block that never would have existed because they'd previously all been living under the same roof.
snvzz 4y ago
>and was sorely disappointed to see Australia cut their funding. An horrible story, covered in detail in Gernot's blog[0]. Fortunately, seL4 foundation has picked up steam, and is no longer dependent in any way on the leeches that almost killed it. [0]. https://microkerneldude.org/ https://microkerneldude.org/

als0 4y ago

> Decades of exploits have me convinced that microkernels are the only real path towards security. Not necessarily. Check out the CHERI project, which has a reasonably good handle on exploits https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/

astrange 4y ago

Australia seems to have a lot of quality CS research (well, that, Mercury, and… WWJDIC), and no way to productize any of it.

im_down_w_otp 4y ago

We at one point created a specialty OS for some exotic network hardware designed for very fancy robots. For a brief period we were using seL4+Ferros like kind of a hypervisor used as the integration point for our "system-level" V&V tools based on what we learned making the aforementioned OS, but we abandoned that approach for non-seL4 reasons. We'll offer something of a "black box recorder" for robots and other cyber-physical systems that's also for runtime verification. Well, seL4 is now managed under a foundation as part of the Linux Foundation umbrella. The seL4 Foundation. Ultimately, I think it might be for the best. Now there are more seL4 researchers and practitioners out in industry working to integrate and build upon seL4 as a building block that never would have existed because they'd previously all been living under the same roof.

snvzz 4y ago

>and was sorely disappointed to see Australia cut their funding. An horrible story, covered in detail in Gernot's blog[0]. Fortunately, seL4 foundation has picked up steam, and is no longer dependent in any way on the leeches that almost killed it. [0]. https://microkerneldude.org/ https://microkerneldude.org/