5 ms·
If I were going through the trouble of writing an adaptable, minimal μkernel, I would start with a capabilities-secure, efficient IPC, formally-verified one lik
by hi-v-rocknroll 2y ago
If I were going through the trouble of writing an adaptable, minimal μkernel, I would start with a capabilities-secure, efficient IPC, formally-verified one like seL4 and then build an NT-compatibility layer. This has a potential advantage of preventing entire classes of vulnerabilities. Finally, if going through such an exercise, might as well write 99.98% of it in Rust to also eliminate numerous traditional categories of frequently-encountered programming errors that oft repeat themselves.
- NetOpWibby 2y agoPlease tell me you're working on this.
- snvzz 2y agoNot him, but multiple such efforts (not necessarily matching your exact description) exist. LionsOS[0] is an effort by the seL4 foundation itself. Makatea[1] is trying to implement a Qubes-equivalent on a safer seL4 base. Genode[2] is an OS framework built around capabilities that supports several microkernels including seL4 itself. 0. https://lionsos.org/ https://lionsos.org/ 1. https://trustworthy.systems/projects/makatea/ https://trustworthy.systems/projects/makatea/ 2. https://genode.org/ https://genode.org/
- NetOpWibby 2y agoDOPE Thanks for sharing!
- snvzz 2y ago>DOPE It's spelt DOpE[0]. 0. https://os.inf.tu-dresden.de/~nf2/dope.html https://os.inf.tu-dresden.de/~nf2/dope.html
- deleted 2y ago[deleted]
- cl91 2y agoGitHub.com/cl91/NeptuneOS Source: I wrote this.