On 7/31/21, Hugo V.C. <skydive...@gmail.com> 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
