[seL4] Re: Operating Systems built on top of seL4

31 Jul 2021

      "Therefore the process server will be almost as important as the kernel
when it comes to security"

I'm not developer, so please excuse my ignorance in some topics (like OS
dev), but, I've experience in exploiting OS stuff and I always prefer a
ring 0 vuln than a ring 3 vuln... If the process server is implemented at
user space (ring 3) then I don't get how we can compare security in so
different cpu execution modes. Am I missing something?

El sáb., 31 jul. 2021 9:38, Andrew Warkentin 
escribió:
...
On 7/31/21, Hugo V.C.  wrote:
...
Hi Andrew,
your project looked interesting to me too so I decided to give it a look
and I coud read here:
https://gitlab.com/uxrt/core-supervisor/sel4-kernel
"The seL4 microkernel with patches for UX/RT"
But my question is: by modifying the seL4 kernel, don't you loose the
security of the formal verification? I mean, the nice thing of a formally
verified code is you can forget about it's security. Don't you fear you
can
introduce vulnerabilities?
Cheers,
The patches are only for the boot code at the moment, which isn't part
of the verification. However, I may end up having to fork seL4 at some
point because the seL4 project's priorities seem to be heavily focused
on static deeply embedded systems rather than desktops, servers, and
large embedded systems.
UX/RT will be extremely centralized in its capability management with
CSpaces, VSpaces, and UTSpaces all managed exclusively by the process
server and no raw seL4 APIs exposed to other processes (the base
standard library will of course call them but the symbols won't be
exported). Therefore the process server will be almost as important as
the kernel when it comes to security. I'd be surprised if it doesn't
end up being way too complex to verify since it will be highly dynamic
and will directly implement (a subset of) the Unix API, which was
never designed with verification in mind, so losing kernel
verification probably won't make much of a difference. Even without
verification, UX/RT should be far more secure than any mainstream OS.
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems