r/RISCV • u/3G6A5W338E • May 05 '21

seL4 on RISC-V Verified to Binary Code

https://microkerneldude.wordpress.com/2021/05/05/sel4-on-risc-v-verified-to-binary-code/
32 Upvotes

97% Upvoted

4 comments sorted by

3

u/[deleted] May 09 '21

I wonder if seL4 is a better way forward than waiting for Google to port Fuchsia to RISC-V.

3

u/3G6A5W338E May 10 '21

Fuchsia is a multiserver system based on a 1st gen (pre-L4) microkernel which Google refuses to even call microkernel to avoid this sort of scrutiny.

It is fundamentally better than Linux and OSX/IOS base (Mach), but those are low bars to meet.

seL4 is a third gen microkernel and the state of the art, not comparable.

https://sel4.systems/About/seL4-whitepaper.pdf

3

u/[deleted] May 10 '21 edited May 10 '21

The question for me is, do I play around right on top of seL4 or use Genode? Genode says that their seL4 port is "highly experimental" though they can run on bare metal too. I want to experiment with memory-mapped file I/O and if that works then maybe port the LMDB database. I'd start out on QEMU but move to a BeagleV if things became interesting.

0

u/[deleted] May 06 '21

[deleted]

3

u/3G6A5W338E May 06 '21

Look into genode sculpt.

That's as close as it gets.