正式な仕様と検証
証明可能な正しいセキュリティモデルを使用してプロトコルを開発することの強みは、敵対的なパワーの限度に関する保証を提供することです。プロトコルが守られ、証明が正しければ、敵対者には、プロトコルのセキュリティ性に違反することができないという約定が与えられます。
より深く洞察すれば、前述の主張の重要性がより明らかになります。敵は予想外に知的かつ有能である場合もあります。数学的モデルだけで彼らの攻撃を防ぎきれるというのは言い過ぎです。それは全く真実ではありません。
現実は、純粋なセキュリティと正常な動作の妨げとなる要因と環境をもたらします。実装が間違っている可能性があります。ハードウェアは、これまで考慮されていなかったベクトルからの攻撃を呼び込む可能性があります。セキュリティモデルが不十分であり、実際の使用に準拠していない可能性があります。
従って仕様、厳重性及びチェックがどれほどプロトコルに要求されているかについての判断が必要となります。例えば、SeL4 Microkernelプロジェクトのような試みは、曖昧さに対する徹底的な攻撃であって、10,000行未満のC言語のコードを検証するために、ほぼ200,000行のIsabelleコードを必要とする主要な例です。しかし、オペレーティングシステムのカーネルは、適切に実装されていないとセキュリティ上の深刻な脆弱性となりうる重要なインフラストラクチャです。
すべての暗号化ソフトウェアは同様の難題に取り組まなければならないのでしょうか。あるいは、同等の成果を生み出すことのできる、それほど厳重ではない手段を選ぶことはできないのでしょうか。また、それが実行されている環境に脆弱性があると悪名高いWindowsXPなどであるならば、プロトコルを完全に実装しようとするのは無意味ではないでしょうか。
カルダノは、以下の点に関して妥協を行いました。まず、暗号技術と分散コンピューティングの複雑な性質のために、検証は非常に繊細で、長く、複雑で、時には至って専門的になる傾向があります。これは、人間によって行われる検査が退屈でエラーを起こしやすくなることを意味します。したがって、コアインフラストラクチャを網羅するために作成されたホワイトペーパーに示されている重要な証明はすべてコンピューターでチェックする必要があると考えています。
次に、Haskellのコードが当社のホワイトペーパーに正確に対応しているかの検証には、LiquidHaskellを介したSMT証明者とのインターフェースとIsabelle/HOLのいずれかを選択することができます。
SMT（充足可能性モジュロ理論）ソルバーは、等式または不等式を満たす関数パラメータを見出す、あるいはそのようなパラメータが存在しないという課題に取り組みます。De MouraとBjørnerが議論したように、SMTの使い道は様々ですが、重要な点は、これらの手法が強力であり、バグやセマンティックエラーを劇的に減らすことができることです。
一方、Isabelle / HOLは、実装の特定と検証の両方に使用できる表現力豊かで多様なツールです。Isabelleは、高次論理構造を扱う包括的な定理ソルバーであり、検証に使用される集合やその他の数学的オブジェクトを表現することができます。そのような制約を伴う問題に取り組むためにIsabelleはZ3 SMT検証システムと統合しています。
どちらのアプローチも有益であるため、両者を段階的に採用することにしました。人間によって記述された検証は、Isabelleでコード化され、その正確性を確認し、それによって我々のシステム化された検査の要件を満たしたことになります。そして、2017年と2018年にかけてカルダノに実装されているすべての本番コードにLiquid Haskellを徐々に追加する予定です。
最後に、正式な検証は、検証している仕様と利用できるツールセットと同じくらい優れています。Haskellを選択する主な理由の1つは、それが実用性と理論の適切なバランスを保っているためです。ホワイトペーパーから得られた仕様は、Haskellのコードによく似ており、この2つを関連づけることは、命令的な言語で行うよりもはるかに容易です。
適切な仕様をキャプチャし、アップグレード、バグ修正などの変更が必要なときに仕様を更新することは未だに困難ですが、それによってHaskellの評価が落ちるようなことはありません。開発者が証明可能安全性の基盤を構築することに苦労しているなら、理論上提案されているものを実装しなければなりません。