haskell - 「安全な言語」で検証済みの SSL/TLS 実装があったとしても、ハートブリード攻撃に対して脆弱でしたか?

Question

ここで著者は次のように主張します。

TLS 仕様を形式化し、実装がそれと一致していることを証明することは、実装が論理的に正しいことを示すだけです。ただし、実装が安全であることは示されません。実装は、論理的には正しくても、サイドチャネル攻撃 (特にタイミング攻撃) に対して脆弱になる可能性があります。

私の質問は次のとおりです。 「安全な言語」(Haskell、Idris) で検証済みの SSL/TLS 実装を使用したり、定理証明者 (Coq、Agda) でチェックしたりしても、ハートブリード攻撃に対して脆弱でしたか?

Answer 1

サイド チャネル攻撃は、たとえばタイミング攻撃です。たとえば、異なる入力を使用したときのタイミングの違いを測定することで、シークレットに関する情報を取得できます。プロセッサの命令、キャッシュ処理、コンパイラの最適化などについて多くの制御を行う C のような低レベル言語でこれを正しく行うことはすでに困難です。高レベル言語でこれを正しく行うことははるかに難しく、それでも十分に効率的です。実際のアプリケーションで使用できるようにします。