解説形式検証：バグがないことを数学的に証明する技術

Published in

Spenge

9 min readMar 15, 2020

概要

Tezosブロックチェーンではよく形式検証による安全性がアピールされます。では、この形式検証は具体的にどのような技術で、どんな安全性を保証できるのでしょうか？ブロックチェーンが形式検証されていればあなたの暗号資産は完璧に安全なのでしょうか？また、どんなことを形式検証すべきなのでしょうか？この記事では形式検証の具体的な理論を簡単に紹介し、技術としての適用範囲と注意点について述べ、これらの問に答えます。

形式検証の目的

形式検証は、ソフトウェアや数学の証明にバグがないことを証明するための技術です。

ソフトウェアにはバグがつきものです。2020年現在の実践的なソフトウェア開発の現場では、テストを行うことでバグがないことを確認するのは必須のことになっています。しかし、テストで本当にバグがないことを保証することはできません。テストで見落とされていたコーナーケースが悪さをするということはよくあります。

数学の証明にもバグがつきものです。数学者が書いた論文の証明が間違っていたということは珍しいことではありません。また、たとえ正しい証明だとしても証明の記述は自然言語で行われるため、解釈間違いが生じたり検証に手間がかかったりします。

形式検証はこのような問題を解決するためのものです。ソフトウェアが仕様を満たしていることや数学の命題が正しいことを、証明記述言語で記述しコンピュータに検証させるのです。以下ではソフトウェアの定理証明支援系による検証の話題に絞って解説することにします。

基礎理論

証明を記述し検証するためには、証明とはそもそも何かという問に真剣に向き合う必要があります。

形式検証を行うためのシステムである証明支援系にはCoq、Lean、Agda、Isabelleや他にもいろいろあります。これらはそれぞれcalculus of inductive construction、Martin-Löf 依存型理論、higher order logicなどの基礎理論に基づいています。

この記事ではTezosの開発言語OCamlと相性の良いCoqに絞って紹介します。

Coqはcalculus of inductive construction（以下CoIC）という基礎理論に基づいた証明支援系です。証明の記述にはCoICに基づいた言語を使います。CoICは型理論の一種です。なぜ型理論が証明と関係するのでしょうか？
それにはカリー・ハワード同型対応が重要な役割を果たします。これは、命題と型、証明とプログラム、証明のカット除去とプログラムの実行がそれぞれ対応するという、証明体系と計算体系の間の不思議な関係です。この対応の下で、命題の証明を書くことと、特定の型を持つプログラムを書くことは等価になります。

カリー・ハワード同型対応の観察

この節では、読者は型にある程度親しみがあるものと仮定します。

A, Bを命題を表す記号とします。また「AならばB」という命題をA -> Bと書くことにします。

今命題Aと命題A -> Bが正しいと分かっているとします。このことからBが正しいと推論することができます。このような推論を次のように書くことにしましょう：

A    A -> B
-----------
B

水平線の上にあるものを前提と呼びます。水平線の下にあるものは結論と呼びます。これがAとA -> Bという前提からBという結論を導く証明です。

具体的に見てみましょう。

Aを「昆虫の脚は6本である」という命題、
Bを「アリの脚は6本である」という命題

とします。A -> Bは「昆虫の脚が6本であるならば、アリの脚は6本である」という命題です。先程の推論は

昆虫の脚は6本である     昆虫の脚が6本であるならば、アリの脚は6本である
------------------------------------------------------------
アリの脚は6本である

となります。

さて、推論の図を観察してみましょう。

A    A -> B
-----------
B

これはプログラムの関数適用の型付け規則と同じ形をしていることに気付きます。aを型Aの値、fを型A -> Bの値（つまりAからBへの関数）とします。するとaにfを適用することでf(a)というB型の値を得ることができます。これを

⊢ a : A    ⊢ f : A -> B
-----------------------
⊢ f(a) : B

と記述します。型の部分に注目すると先程の推論と同じです。これが「命題=型」とみなすことができるという状況証拠の一つです。他にもペア型A * Bは「AかつB」という命題に対応するなど、各型構成子が命題の世界における対応物を持ちます。また、aやf、f(a)は証明の構造に相当する情報が保存されています。これが証明をプログラムとみなすことができるという事実です。

厳密には、単純型付きラムダ計算が直観主義論理に対応するというのが一番簡単なカリー・ハワード同型対応です。より複雑な仕様を記述するには「すべてのxについて・・・」や「あるxが存在して・・・」という量化の取り扱いが欲しくなってきます。こういう体系に対応する計算体系が依存型のあるラムダ計算です。その一種がcalculus of constructionです。これに帰納型という型の構成を付け加えたものがCoqの基礎理論calculus of inductive constructionです。興味があればここで登場したキーワードでさらに調べてみてください。

Coqの入門としてはSoftware Foundationsがおすすめです。

ソフトウェアの検証方法

Coqを用いてOCamlで書かれたソフトウェアを形式検証するときのよくある手順を紹介します。

1. ソフトウェアのうち検証したい部分を抜き出す。
2. その部分を Coq のプログラムとして記述する。
3. 検証したい性質を命題（=型）として記述する。
4. その性質の証明（=プログラム）を記述する。
5. Coqで証明の正しさ（=プログラムに正しく型がつくか）を検査する。
6. CoqのプログラムからOCaml言語へ「プログラム抽出」を行う。
7. 抽出されたプログラムをもとのソフトウェアの部分に戻す。

このように形式検証には多くのステップがかかります。またひとつのステップに要する時間も、同じ量の通常のプログラム記述より多大になります。そのため、本当に重要な部分に絞って検証することや、検証しやすいソフトウェア設計を行うことが重要です。検証済みプログラムをライブラリ化することも重要です。

また検証しやすいプログラミング言語というものもあります。OCamlはCoqと非常に相性がよく（CoqはOCamlで開発されています）、比較的楽に検証できます。筆者はあまり詳しくありませんがHaskellやScalaも環境がある程度整っているようです。

例を考えましょう。ブロックチェーンアプリケーションのある操作の前後で資金の量が変わらないことを証明したいとしましょう。仕様は（操作前の資金量）=（操作後の資金量）という式をCoqの言語で書いたものになります。この仕様を満たすことを1–7のステップで検査すれば、あなたのアプリケーションはその操作の最中に資金を盗まれないことが保証されたことになります。

形式検証で何ができないか

「全てのバグを、生まれる前に消し去りたい。全ての宇宙、過去と未来の全てのバグを、この形式検証で」

この有名な願いが叶う日は来るのでしょうか？残念ながらその願いは叶いません。

形式検証ではプログラムが仕様通りになっていることを証明できます。ではその仕様にバグがないことはどうやって保証するのでしょうか？この保証は完全には不可能です。例えば、あなたが暗号資産を受け取るプログラムが欲しいときに、間違って送る仕様を書いてしまったとしましょう。その仕様通りのプログラムを書き実行した場合、あなたは自分の暗号資産が安全に他人に送られてしまうことに気づくでしょう。ただし、証明中に仕様の誤りに気付く可能性は高まります。意図したプログラムを書いているのに証明がなかなか書けない場合は仕様のミスの可能性があります。

また、仕様にない挙動を保証することもできません。例えば送金プロトコルが数学的に安全であることを証明したとします。しかし仕様に記述していなかった思わぬサイドチャネル攻撃などの危険は防げません。

矛盾した仕様を満たすプログラムを書くことも不可能です。なぜか証明がうまくいかないと思ったら仕様自体の矛盾がないか疑ってみるのも重要なことです。

証明も反証もできないことが証明されている命題の証明・反証も当然ながら不可能です。例えばゲーデルの不完全性定理より、「十分強力な」定理証明支援系それ自体の無矛盾性を（その定理証明支援系が無矛盾である限り）その定理証明支援系の中で（公理を追加することなく）証明することは不可能です。

形式検証を行う場面とブロックチェーン

形式検証はこれまで、航空宇宙、原子力、防衛、半導体、医療機器、自動運転、金融などの領域に適用されてきました。これらの領域ではソフトウェアのバグが人命や莫大な資金の喪失につながるため、形式検証のコストは十分受け入れられるものです。また、そうでなくてもよく使う関数を形式検証しライブラリ化すればコストにみあう効果を得られるでしょう。

ブロックチェーンもそのような性質を持つ金融領域のアプリケーションとして安全性に十分注意を払うべきです。実際、ブロックチェーン上の分散金融アプリケーション(DeFi)からの資金流失は近頃毎月のように起こっています。

Tezosブロックチェーンでは形式検証しやすいスマートコントラクト言語を採用しています。このことから今後のDeFiはTezosでも活発になることが予想されますし、我々も活発にしていきたいと思っています。またDeFi以外のブロックチェーンアプリケーション（例えばゲームや流通管理）でも形式検証は依然として重要です。そこでも我々の技術で安全なアプリケーションを実現したいと考えています。

まとめ

証明支援系の具体的な基礎理論（のほんのアイデアの一部ですが）を紹介し、Coqではカリー・ハワード同型対応が本質的であることを見ました。
ブロックチェーンアプリケーションで資金が盗まれないことを保証することができるという例を紹介しました。また、形式検証が万能な魔法ではないことも注意点として紹介しました。ブロックチェーンは形式検証の適用領域としてまさにふさわしいものだということをDeFiにおける資金流出事件を例として示しました。