3 ms·

Create a secure POSIX-compatible userland on top of seL4. This goal fills me with nerd lust. Getting ourselves a secure foundation to build on doesn't solve al

Create a secure POSIX-compatible userland on top of seL4. This goal fills me with nerd lust. Getting ourselves a secure foundation to build on doesn't solve all our problems (not by a long shot), but such a drastic reduction in attack surface would be an incredible achievement.

mwcampbell 11y ago
Then add NetBSD drivers as rump kernels to get it running on real hardware. True, drivers in Rust would be even better, but IIUC, the whole point of using a microkernel is that the drivers would be running in user space with restricted privileges.
- nickpsecurity 11y ago
  It helps in fault containment which helps availability primarily. Without IOMMU, they still can wreak havoc. So, drivers shown to be safe is still beneficial. I've so far seen that done with Ada/SPARK, w/ static analysis, Java w/ driver partly in JVM, and most recently ATS language. Rust would make a nice experiment.
  - Scramblejams 11y ago
    Not just that, but I worry about IOMMU bugs. A safe driver would help mitigate those.
    - nickpsecurity 11y ago
      Good point. Few think about that. Hardware will periodically fail, especially on deep-submicron processes.
gioele 11y ago
>> Create a secure POSIX-compatible userland on top of seL4. > > This goal fills me with nerd lust. I remember a L4 talk in which the speaker showed how more than 95% of the code of new OSes where devoted to being POSIX compatible and yet they 1) lacked a lot of features 2) missed many edge cases 3) had to modify their beautiful kernel design to accommodate POSIX use cases. I think the only way forward is to do like Plan9 did. Just forget about POSIX and implement your own set of primitives (but first study what has been done in the last 40 years!). POSIX compatibility can come later with 80/20 library that maps POSIX calls and behaviour to the new primitives. And maybe POSIX is not needed at all. If your OS is interesting enough people will add #ifdef'd code for your platform, just like many UNIX-y applications do now for Android, OS X or Windows.
- comex 11y ago
  FWIW, OS X is UNIX 03 certified: http://www.opengroup.org/openbrand/register/brand3612.htm http://www.opengroup.org/openbrand/register/brand3612.htm Android, for these purposes, is, of course, Linux with a different libc, so most of the POSIXy stuff is there, even if bionic is pretty awful.

mwcampbell 11y ago

Then add NetBSD drivers as rump kernels to get it running on real hardware. True, drivers in Rust would be even better, but IIUC, the whole point of using a microkernel is that the drivers would be running in user space with restricted privileges.

nickpsecurity 11y ago
It helps in fault containment which helps availability primarily. Without IOMMU, they still can wreak havoc. So, drivers shown to be safe is still beneficial. I've so far seen that done with Ada/SPARK, w/ static analysis, Java w/ driver partly in JVM, and most recently ATS language. Rust would make a nice experiment.
- Scramblejams 11y ago
  Not just that, but I worry about IOMMU bugs. A safe driver would help mitigate those.
  - nickpsecurity 11y ago
    Good point. Few think about that. Hardware will periodically fail, especially on deep-submicron processes.

gioele 11y ago

>> Create a secure POSIX-compatible userland on top of seL4. > > This goal fills me with nerd lust. I remember a L4 talk in which the speaker showed how more than 95% of the code of new OSes where devoted to being POSIX compatible and yet they 1) lacked a lot of features 2) missed many edge cases 3) had to modify their beautiful kernel design to accommodate POSIX use cases. I think the only way forward is to do like Plan9 did. Just forget about POSIX and implement your own set of primitives (but first study what has been done in the last 40 years!). POSIX compatibility can come later with 80/20 library that maps POSIX calls and behaviour to the new primitives. And maybe POSIX is not needed at all. If your OS is interesting enough people will add #ifdef'd code for your platform, just like many UNIX-y applications do now for Android, OS X or Windows.

comex 11y ago
FWIW, OS X is UNIX 03 certified: http://www.opengroup.org/openbrand/register/brand3612.htm http://www.opengroup.org/openbrand/register/brand3612.htm Android, for these purposes, is, of course, Linux with a different libc, so most of the POSIXy stuff is there, even if bionic is pretty awful.