haskell - 如果以“安全语言”进行验证的 SSL/TLS 实施，它仍然容易受到心脏出血攻击吗？

Question

在这里，作者提出了主张：

将 TLS 规范形式化并证明实现与它一致仅表明该实现在逻辑上是正确的。但是，它并不表明实现是安全的。您的实现可能容易受到旁道攻击（特别是定时攻击），同时仍然在逻辑上是正确的。

我的问题是：如果使用“安全语言”（即 Haskell、Idris）或使用定理证明器（Coq、Agda）进行了验证的 SSL/TLS 实现，它仍然容易受到 heartbleed 攻击吗？

Answer 1

侧信道攻击例如是定时攻击，例如，您可以通过测量使用不同输入时的定时差异来获取有关秘密的信息。在像 C 这样的低级语言中已经很难做到这一点，在这种语言中，您可以对处理器指令、缓存处理、编译器优化等进行大量控制。在高级语言中正确地做到这一点要困难得多——并且仍然足够高效可以在实际应用中使用。