如果使用“安全语言”进行了经过验证的 SSL/TLS 实施，它仍然容易受到 Heartbleed 攻击吗？

Question

作者在此提出主张：

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

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

Answer 1

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