The SeL4 FAQ has this gem I'm struggling to say what's wrong with that claim from a scientific POV. As others also point out, security is conditional on vario

The SeL4 FAQ has this gem I'm struggling to say what's wrong with that claim from a scientific POV. As others also point out, security is conditional on various things, including, in this case, what you consider a valid flow of information and what you don't. For example if an OS allows user-mode to read AES-encrypted kernel-mode data then that would be insecure if you had an unrestricted attacker (who can brute-force AES) but secure assuming polynomial attackers (under standard hardness assumptions for AES). To add insult to injury, we don't in fact know if the standard hardness assumptions actually hold for AES.