> I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal. Not sure how difficult this is for good "safe" languages such as e.g. Haskell.
I wonder if optimizations affect the area of code that would need to be verified? Haskell is pure, and this fact is exploited in a lot optimizations and code generation - I guess one would have to prove that all of these transformations preserve the integrity of the Haskell semantics.
I guess you could have a small (compared to GHC) implementation of Haskell which is formally verified, which is small because you don't bother with hardly any optimizations?
Side-channel attacks are my primary concern with writing secure code. For example, if Haskell optimizes and makes some decryption functions run faster than others for an attacker-chosen ciphertext, the attacker could use the runtime differences perform a timing attack [1], and potentially learn your secrets.
I wonder if optimizations affect the area of code that would need to be verified? Haskell is pure, and this fact is exploited in a lot optimizations and code generation - I guess one would have to prove that all of these transformations preserve the integrity of the Haskell semantics.
I guess you could have a small (compared to GHC) implementation of Haskell which is formally verified, which is small because you don't bother with hardly any optimizations?