It’s fundamentally full of concepts incompatible with capability based security principles, which are provably secure. Access control lists are provably insecur

It’s fundamentally full of concepts incompatible with capability based security principles, which are provably secure. Access control lists are provably insecure. POSIX resource management is archaic. It’s not possible to define “ownership” clearly on a Unix system. You could certainly write a Unix abstraction layer on top of seL4, or more commonly treat seL4 as a hypervisor, but you would not be able simply use a Unix interface to interact with seL4 and get all of it’s benefits. Capability based systems don’t magically carry their desired properties up the abstraction ladder, they have to be maintained and the designer has to be vigilant to avoid introducing ambient authority by using capability based design themselves. Genode is an example of a layer over seL4 that follows these principles.