3 ms·
seL4 is a system formally verified up to machine code. https://sel4.systems/About/home.pml https://sel4.systems/About/home.pml It won't protect you against un
by danuker 4y ago
seL4 is a system formally verified up to machine code.
https://sel4.systems/About/home.pml https://sel4.systems/About/home.pml
It won't protect you against unprotected apps doing what they want, nor against CPU backdoors, but it reduces your attack surface by a lot.
- atemerev 4y agoShould we trust a formal verifer program which was used to verify seL4? (Remember: being "open source" does not help in such cases).
- danuker 4y agoI suppose a trojan designed for a specific compiler is hard enough to make. Having it hijack a model checker as well, in order to conceal itself from resulting models, would be a giant leap more difficult. So, you are still risking it if you have nation-state adversaries, but not if they are script kiddies.