Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.


GitHub.com/cl91/NeptuneOS

Source: I wrote this.


Please tell me you're working on this.


Not 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/

1. https://trustworthy.systems/projects/makatea/

2. https://genode.org/


DOPE

Thanks for sharing!





Consider applying for YC's Fall 2026 batch! Applications are open till July 27.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: