Makatea: Qubes-like OS on seL4

https://www.trustworthy.systems/projects/TS/makatea


See also earlier topics about alternative operating systems

Qubes-lite With KVM and Wayland
and

Spectrum OS discussion

and

BastilleBSD discussion

and

Bottlerocket

3 Likes

See also:

That’s about what I suggested some time earlier in issue #3894 ‘Use verified L4 kernel instead of Xen’. I hope they get along with that, and in close cooperation with Qubes!

3 Likes

The reason it is Qubes-like, rather than being a full Qubes OS port, is that it is limited to server-side uses where all VMs are defined in a compile-time configuration file. Obviously this is not sufficient for the desktop use-cases that Qubes OS targets. I both hope and believe that Qubes OS can and will be ported to seL4 at some point, but this will require substantial development effort.

4 Likes

SEL4 + Qubes is game changer

But unsw been talking about this for 10 years

1 Like

Xen is about 100k lines of code, and sel4 is about 10000 lines of code. Why someone who is ‘paranoid’ enough to treat their threat models from government agency, in a security sense, would bother use homomorphic encryption to the raw data of their sel4 kernel? Also, I wonder if xen is encryptable by homomorphic encryption(I heard that the most challenging part of that encryption is encryption speed).

link doesnt work, please update it as its interesting