"I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal." Proving all layers logically correct

"I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal." Proving all layers logically correct would be a great start :) We could probably have avoided this whole Heartbleed debacle. If you'll allow me to elaborate on the security properties, it's worth pointing out that even if your TLS implementation ran on top of a formally-proven correct VM and used formally-proven correct libraries, and ran on a formally-proven correct kernel and processor, you still have to prove that it resists side-channel attacks before it can be said to be secure. Doing so is open-ended, and likely impossible, since side-channel attacks come in all shapes and sizes, and some are outside the scope of software engineering. For example, how do we prove that a logically-correct TLS implementation is secure against acoustic analysis? [1] How would we have done this before it was known that acoustic analysis was possible? This is the essence of what makes writing secure code hard. [1] https://www.cs.tau.ac.il/~tromer/acoustic/ https://www.cs.tau.ac.il/~tromer/acoustic/