Had a verified SSL/TLS implementation in a 'safe language' would it still have been vulnerable be to the heartbleed attack? [closed]

Question

Closed. This question needs details or clarity. It is not currently accepting answers.

---

Want to improve this question? Add details and clarify the problem by editing this post.

Closed 9 years ago.

Improve this question

Here the author makes the claim:

Formalizing the TLS specification and proving that an implementation is consistent with it only shows that the implementation is logically correct. However, it does NOT show that the implementation is secure. Your implementation can be vulnerable to side-channel attacks (particularly timing attacks) while still being logically correct.

My question is: Had a verified SSL/TLS implementation in a 'safe language' (ie Haskell, Idris) or checked with a theorem prover (Coq,Agda) would it still have been vulnerable be to the heartbleed attack?

Answer 1

Side channel attacks are for instance timing attacks, e.g. you can get information about the secrets by measuring timing differences when using different inputs. It is already hard to do this right in a low level language like C where you have lots of control about processor instructions, cache handling, compiler optimizations etc. It is much harder to do this correctly in higher level languages - and be still efficient enough to be usable in real-world applications.