<分区>
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.
我的问题是:如果使用“安全语言”(即 Haskell、Idris)或使用定理证明器(Coq、Agda)验证过 SSL/TLS 实现，它是否仍然容易受到攻击？攻击？
最佳答案
侧信道攻击是例如定时攻击，例如您可以通过测量使用不同输入时的时间差异来获取有关 secret 的信息。在像 C 这样的低级语言中已经很难做到这一点，在这种语言中，您可以对处理器指令、缓存处理、编译器优化等进行大量控制。在高级语言中正确地做到这一点要困难得多——而且仍然足够高效可用于实际应用。
关于haskell - 如果在 'safe language' 中实现了经过验证的 SSL/TLS，它是否仍然容易受到心脏出血攻击？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/23084610/