1. 17

  2. 4

    Can’t GenodeOS work as the userland for seL4?

    1. 5

      Genode is nice and all, but it is Affero GPL licensed. This is likely seen as a huge liability.

      1. 5

        Specifically because they want hardware/software businesses to pay for using it. So, they should probably think of that combo as seL4 plus a commercial product. Most won’t use it as you predicted.

        1. 4

          Ooooh, now that is something I totally missed, thanks!

        2. 2

          From their documentation 1:

          Genode can be deployed on a variety of different kernels including most members of the L4 family (NOVA, seL4, Fiasco.OC, OKL4 v2.1, L4ka::Pistachio, L4/Fiasco). Furthermore, it can be used on top of the Linux kernel to attain rapid development-test cycles during development. Additionally, the framework is accompanied with a custom microkernel that has been specifically developed for Genode and thereby further reduces the complexity of the trusted computing base compared to other kernels.

          1. 2

            But seL4 is single core only, so it’s not much use outside of embedded or single-purpose equipment :(

            1. 1

              Uh, oh :/ this is something I didn’t realize :(

              1. 1

                They have an unverified implementation, which is roughly as secure as a normal operating system.