2 ms·
>SeL4 has a fully verified kernel but it doesn't do virtualization yet. It very much does virtualization. And, as far as I am aware, it does it better than any
by snvzz 2y ago
>SeL4 has a fully verified kernel but it doesn't do virtualization yet.
It very much does virtualization. And, as far as I am aware, it does it better than any other OS.
Incidentally, seL4 just had its seL4 Summit 2024[0].
0. https://www.youtube.com/playlist?list=PLtoQeavghzr0ZntMmRPwg1VA1yJd_T3y9 https://www.youtube.com/playlist?list=PLtoQeavghzr0ZntMmRPwg...
- throwaway48476 2y agoBut is the virtualization component fully verified?
- snvzz 2y agoThere are a few talks on VMM. The major shortcoming right now is that guests only get one CPU, but as per the talks guest SMP is a priority and will be available in 3-4 months. I do not follow the verification side much, but what I know is that VMM has some interesting properties. Namely, VMM itself (which handles VM exceptions) does not get more capabilities than the VM, thus dramatically limiting usefulness of a VM escape.
- ruthmarx 2y agoDo you have links for some of the latest development/research on this?