3 ms·
Should we trust a formal verifer program which was used to verify seL4? (Remember: being "open source" does not help in such cases).
by atemerev 4y ago
Should 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.