3 ms·

Wouldn't that be cool? Another neat idea would be to build on an existing microkernel like seL4, but write the userspace -- all the drivers, memory manager, fi

Wouldn't that be cool? Another neat idea would be to build on an existing microkernel like seL4, but write the userspace -- all the drivers, memory manager, filesystems, etc -- in Rust. The NICTA team already has proofs of correctness for the microkernel itself, so why reinvent the wheel? But at the same time, those proofs were super expensive and difficult to make. It would be awesome if we could get a reliable userland more easily by using a better language. I wonder what it would take to get Rust compiling for seL4?

nanolith 11y ago
Not much, really. The main thing needed is to port the language runtime to seL4. This should be a relatively small effort, and a great project to both learn some of the underbelly of Rust's ABI and seL4.
- cmrx64 11y ago
  Already done :)
  - nanolith 11y ago
    I saw a sibling reply posted shortly before mine outlining your work. Nice job. :-)
vitno 11y ago
I've helped work some on a project doing that right now, although it's mostly been the awesome cmr. https://gitlab.com/robigalia/sel4-sys https://gitlab.com/robigalia/sel4-sys
serge2k 11y ago
> why reinvent the wheel Why not.
- cmrx64 11y ago
  It's /only/ 30 man years of effort from experienced engineers. http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A... page 56.
cmrx64 11y ago
You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope to have a release of the foundational libraries sometime in the next two weeks. There's a mailing list, if you want to watch: https://lists.robigalia.org/listinfo/robigalia-dev https://lists.robigalia.org/listinfo/robigalia-dev And the (still in-progress) source code: http://gitlab.com/robigalia/sel4-sys http://gitlab.com/robigalia/sel4-sys. I have some ideas about encoding RPC protocols as DFAs in Rust's type system, and then doing verification of the protocols in a more abstract setting (perhaps NuSMV or a similar checker). This is somewhat similar to the (ancient at this point) "protocol compiler" that used to be in Rust, doing a similar thing for channels. I'm interning at Data61 (née NICTA) on the verification team starting Jan 18, and I'm hoping to transfer some of that experience and knowledge into verifying Rust.
- nanolith 11y ago
  I would love to see some blog posts regarding your experience during this internship. I am working on some formal verification myself for some commercial projects, and I enjoy reading about stuff like this.
- xj9 11y ago
  Dream come true!
- cvwright 11y ago
  Excellent! Thank you for your work on this. I'll be very excited to see where it goes.

nanolith 11y ago

Not much, really. The main thing needed is to port the language runtime to seL4. This should be a relatively small effort, and a great project to both learn some of the underbelly of Rust's ABI and seL4.

cmrx64 11y ago
Already done :)
- nanolith 11y ago
  I saw a sibling reply posted shortly before mine outlining your work. Nice job. :-)

vitno 11y ago

I've helped work some on a project doing that right now, although it's mostly been the awesome cmr. https://gitlab.com/robigalia/sel4-sys https://gitlab.com/robigalia/sel4-sys

serge2k 11y ago

> why reinvent the wheel Why not.

cmrx64 11y ago
It's /only/ 30 man years of effort from experienced engineers. http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A... page 56.

cmrx64 11y ago

You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope to have a release of the foundational libraries sometime in the next two weeks. There's a mailing list, if you want to watch: https://lists.robigalia.org/listinfo/robigalia-dev https://lists.robigalia.org/listinfo/robigalia-dev And the (still in-progress) source code: http://gitlab.com/robigalia/sel4-sys http://gitlab.com/robigalia/sel4-sys. I have some ideas about encoding RPC protocols as DFAs in Rust's type system, and then doing verification of the protocols in a more abstract setting (perhaps NuSMV or a similar checker). This is somewhat similar to the (ancient at this point) "protocol compiler" that used to be in Rust, doing a similar thing for channels. I'm interning at Data61 (née NICTA) on the verification team starting Jan 18, and I'm hoping to transfer some of that experience and knowledge into verifying Rust.

nanolith 11y ago
I would love to see some blog posts regarding your experience during this internship. I am working on some formal verification myself for some commercial projects, and I enjoy reading about stuff like this.
xj9 11y ago
Dream come true!
cvwright 11y ago
Excellent! Thank you for your work on this. I'll be very excited to see where it goes.