From the assumptions page: http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml ``` Hardware: we assume the hardware works correctly.

From the assumptions page: http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml ``` Hardware: we assume the hardware works correctly. In practice, this means the hardware is assumed not to be tampered with, and working according to specification. It also means, it must be run within its operating conditions. Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels ``` Rowhammer and Spectre exploits hardware not working to spec. These sorts of attacks using heretofore "unreasonable" exploitation of side-channel and hardware vulnerabilities are exactly what worries me. We have no solutions for these classes of attacks. Complex high-speed systems are still inherently unsolvably vulnerable, it seems.