フォーマル検証（Formal Verification）手法は、その誕生以来、「ニッチ、不人気」などの言葉と関連付けられてきました。正式な検証方法は「軍事レベルの」ハッキング対策方法であると言う人もいますが、それがこのテクノロジーに謎を加えています。

正式な検証方法とは具体的に何ですか?

Wikipedia では形式的検証について次のように説明しています。

コンピューター ハードウェア (特に集積回路) およびソフトウェア システムの設計プロセスにおいて、形式的検証の意味は、数学的手法を使用して、1 つまたはいくつかの形式的な仕様または特性に従ってその正確性または不正確性を証明することです。

この謎の感覚は、おそらく、定義に含まれる 2 つの厳密かつ抽象的なキーワード、「形式仕様」と「数学的手法の証明」から来ていると考えられます。実際、この謎の層を明らかにすると、形式的検証の多くの興味深い側面が見つかるでしょう。

次の記事で私が議論したい質問は次のとおりです。現時点で、次のストーリーのうち、形式的検証に対するあなたの想像力を本当に満足させることができるのはどれですか?形式的検証は本当にブロックチェーン分野のテクノロジーとして普及できるのでしょうか?もしそうなら、どうやってそれを行うことができますか？

（追記：上記の「形式仕様」の概念については後述します。）

上記の質問に答えるために、まず別の簡単な質問を考えてみましょう。

>この段階で、人々は何のために形式的手法を使用するのでしょうか?

この質問に対する答えは 2 つだけです。

>1. 間違いを避ける

>最初のレベルのタイトル

| 間違いを避ける

間違いを避けることは、実は損失を避けることなのです。

まず、プログラミング エラーが許容されない領域はどの領域でしょうか?プログラミングエラーによる損失が計り知れないのはどの分野ですか?

実際、形式的手法はハードウェア設計の頃から普及してきました。有名な例は、Intel の Pentium CPU 浮動小数点ユニットでエラー (FDIV バグ) が発生し、数万個の CPU をリサイクルして交換する必要があり、Intel に多大な損失 (4 億 7,500 万ドル) をもたらした[1] です。

それ以来、インテルはチップ設計に正式な手法を広範囲に採用してきました。

IBM、AMD、NVIDIA、CADENCE[2] などのコンピューター ハードウェアの大手企業も、形式的手法のユーザーです...

溝を掘れば多くの知恵が得られると言うのは、実は各界で試行錯誤している人がいて、それは産業界でも同じです。例: 1996 年、欧州宇宙機関のアリアン 5 (アリアン 5) ロケットの最初の打ち上げでは、慣性航法システムによって送信された誤ったコマンド (オーバーフローを引き起こす浮動小数点数が整数に変換された) により、ロケットは打ち上げのみに終わりました。 37秒間走行した後、所定の軌道を逸脱し、最終的に墜落した。欧州宇宙機関の巨額の研究開発資金(80億ドル)[3]が炎上した。

その後間もなく、EADS は正式な手法を使用して、アリアン ロケットのミッション スケジュール モデルを開発し始めました。

アメリカ航空宇宙局 NASA と英国国防省は 1990 年代に相次いで設計基準を発行し [4]、その中には形式的な手法の使用が列挙されていました。我が国の Yutu 月面探査機制御システムと我が国初の自社開発宇宙船組み込みリアルタイム オペレーティング システム SpaceOS[5] も、正式な方法を通じてその正しさを検証しています。

歴史の発展は、お金が社会発展を促進する最初の原動力であることを示しています。プログラムエラーによって引き起こされる巨額の損失を嘆く余裕は誰にもありません。

上記の 2 つの話が重すぎるように聞こえる場合は、次の図を見てみましょう。

上の図は、正式な手法を使用して開発された地下鉄プロジェクトの世界的な分布を示しています[6]。

パリの地下鉄信号システムを皮切りに、北米、ヨーロッパ、アジア、南米の一部の主要国の地下鉄システムの開発に形式的手法が広く使用されていることがわかります。地下鉄の故障による大規模な損失や災害がほとんど聞かれないのはそのためだろう。

繰り返しますが、お金は主要な生産力です。

日常の移動を保証するための形式的手法の貢献が広く認識されている現在、ブロックチェーン技術に基づいて開発されたデジタル資産の分野では、形式的検証技術をスマートコントラクトの安全性を確保するために使用し、それによって財産を保護することができるという考えです。セキュリティは合理的かつ緊急なものになります。

どうすればいいですか？ここで簡単に紹介します。

まず、「形式仕様」という概念を導入する必要があります。

正式仕様 (正式仕様) とは、システムの予期される動作 (アカウント A からアカウント B に多数の S トークンを転送するなど) とプロパティ (転送によってアカウント B のオーバーフローが発生しないなど) の厳密かつ包括的な実装を指します。 ) 数学的言語による定義。多くの場合、正式な仕様はシステムの正確性とセキュリティを定義します。

システムの正式な仕様が与えられると、その仕様から始めてシステムを反復的に設計および実装できます。反復の各ステップでは、改良、合成、形式的証明などの一連の方法を通じて、反復によって生成されたシステムが反復前の仕様またはシステムと一致していることを数学的に厳密に保証できます。

形式仕様に基づいてシステムを設計および実装することに加えて、シンボリック実行、モデルチェック、形式証明を含む一連の方法を使用して、既存の設計と実装がこの仕様と一致していることを検証することもできます。

壮大そうに聞こえますよね？

たとえば、スマート コントラクト プログラムの場合、各ステートメントのセマンティクスに従って、考えられるすべての入力 (関数パラメーターの組み合わせなど) と初期状態 (状態変数の初期値の組み合わせなど) から開始できます。 、文ごとにプログラムの考えられるすべての終了状態 (状態変数の値やコントラクト実行後に生成されるイベント ログなど) を推定し、すべての入力、初期状態、終了状態の組み合わせが正しいかどうかを確認します。契約は正式な仕様と一致しています。これは、コナンが段階的に事件を解決したのと少し似ています。ただし、ここでのすべての定義は厳密な数学的言語で説明されており、導出と検査も厳密な数学的導出と証明です。検証するシステムの複雑さとその正式な仕様に応じて、導出と証明は手動で構築することも、機械によって自動的に生成することもできます。

最初のレベルのタイトル

| 攻撃に対して

敵対的攻撃は、実際には損失を回避するための別の意味です。

物語は米軍による電子攻撃から始まる。 2015年の夏、あるハッカーが米軍の無人ヘリコプター「リトルバード」への電子攻撃を命じられ、ドローンを制御した。しかし、米国国防総省が UAV の中核制御プログラムを再開発したとき、ハッカーは今日世界中のあらゆる攻撃方法を使用しましたが、新たに配備されたシステムを突破することはできませんでした [7]。

あらゆる攻撃を防ぐ超防御力をリトルバードに与えた技術とは？答えは、正式な検証方法です。

形式的検証手法は、厳密な数学的証明を通じてプログラムの動作が期待と一致していることを保証しますが、形式的検証プログラムの正しさには非常に労力がかかるため、プログラム テストなどの汎用手法とは異なり、形式的検証手法はセキュリティにのみ適用されることがよくあります。ドローン、宇宙船、オペレーティング システムなどのプログラムの正当性検証などの重要な領域。

ここで言及しなければならないのは、2016 年に発見された Linux オペレーティング システムのカーネルの非常に深刻な脆弱性である Dirty Cow (CVE-2016-5195)[8] です。攻撃者はこの脆弱性を利用してシステムの最高の特権を取得し、システム全体が使用状態ではシステムが悪用される可能性があります。

最初のレベルのタイトル

| セキュリティクリティカルなブロックチェーン分野

ブロックチェーンの分野でも同様で、小さなミスが大きな損失につながる一方で、多大な経済的利益が多数の攻撃者を引き寄せる可能性もあります。

最初の大規模なイーサリアム ハッキング事件である The DAO では、攻撃者は当時 5,500 万ドル相当のイーサリアムを盗み、これがイーサリアムのハードフォークにつながりました[11]が、その後もイーサリアムのスマート コントラクトに関連した攻撃が続いています。 , 2017年11月、イーサリアムパリティウォレットがハッキングされ、ユーザーは約1億5,000万ドル相当のデジタル資産を失いました[11]。

Ambi Labs の統計によると、2018 年上半期だけで約 11 億ドルのデジタル資産が盗まれ、ブロックチェーン システムに関連する脆弱性 (イーサリアムのスマート コントラクトの脆弱性など) やデジタル資産を取り巻くエコシステムのセキュリティ問題 (たとえば、複数の集中型取引所の盗難など）が際限なく出現しています。

現時点では、ブロックチェーン システムの関連する抜け穴とデジタル資産エコシステムのセキュリティ問題は、最終的には関連プログラムの設計と実装に関連しています。正式な手法が導入される前は、このような問題は主にプログラムのテストを通じて発見されていました。

形式的検証がブロックチェーン分野に参入した初期の頃、イーサリアム コミュニティの平井洋一は、イーサリアムのスマート コントラクト仮想マシン EVM の完全な形式的モデリングを行いました。さらに、UIUC 大学のチームも EVM を正式にモデル化して検証しました [12]。 EVM はイーサリアム スマート コントラクトの基礎となるコアであり、イーサリアムのセキュリティに関連しており、コミュニティからの幅広い注目を集めているデジタル資産保護などの重要な問題を含んでいます。

さらに、MakerDAO プロジェクトは、最初の正式に検証された分散型アプリケーション (DApp) をリリースしました [13]。 MakerDAO は、ステーブルコイン、担保ローン、分散型コミュニティ ガバナンス機能を提供するイーサリアム ベースのスマート コントラクト プラットフォームです。導入されたスマートコントラクトのセキュリティを確保するために、MakerDAOチームはK-Framewokを通じて住宅ローン（CDP）のコアエンジンコントラクトのコントラクトコードを検証し、スマートコントラクトプログラムがハッカー攻撃に完全に対抗できることを示しました。

Ambi Labs は、イーサリアム スマート コントラクトの正式な検証についても多くの作業を行い、スマート コントラクトの正式な検証フレームワークを提案し、ERC20、ERC721 などのこのフレームワーク内のいくつかの一般的なトークン コントラクト (一般的な機能を含む) を証明しました。転送、トークンの合計金額など）。これらの数学的に証明されたスマート コントラクトは、セキュリティの問題を心配することなく直接使用できます。これらの契約ソース コードと証明プロセスは、オープン ソースの形式でコミュニティに提供されています [14]。

最初のレベルのタイトル

https://github.com/sec-bit/tokenlibs-with-proofs

| 結論

形式的検証手法というと意味が分からないと思われがちですが、それは形式的検証手法が一般的な技術ではなく、現場と組み合わせることでその価値を発揮できる特殊な技術だからです。ブロックチェーンの分野において、形式的手法があると便利か、なければならないかは、プロジェクトの特性と切り離すことができません。

ブロックチェーン技術とプロジェクトアプリケーションの探求が深化し続けるにつれて、間違いを回避し、ハッカー攻撃に抵抗し、財産の損失を回避したいというプロジェクト当事者の要求はますます強くなってきています。

最初のレベルのタイトル

最後に書かれています | 検証とテストの関係についてどれくらい知っていますか?

最後に、正式な検証とテストの関係について話しましょう。

「プログラムのテストはエラーの存在を証明できますが、エラーがないことを証明することはできません。」 Edsger Dijkstra (1972 年のチューリング賞受賞者、形式手法の中核となるアイデアの提案者) は次のようにコメントしています。

実際には、特にコードが十分に複雑なシナリオでは、形式的検証 (Verification) とプログラム テスト手法 (Testing) の検証効果は雲と泥のように異なります。

例: 2009 年、オーストラリアの科学者は正式な手法を使用して、産業グレードのオペレーティング システムの seL4 マイクロカーネルの完全な機能検証を実施しました [15]。検証手法は、形式的な検証とプログラム テストの 2 つの方法で実行されました。検証の結果、形式的手法では460以上のバグが発見されたが、プログラムテストでは16のみのバグが発見された。

さらに興味深いのは、検証コストが高いことで知られる形式検証の分野において、seL4 マイクロカーネルを完全に検証する検証コストはわずか 600 万米ドルであるのに対し、テストによって CC EAL6 認定に合格するコストは 87 ドルにも上ることです。 100万米ドル [15]。

正式な検証により、seL4 マイクロカーネルの強力なセキュリティ保証をより経済的に提供できることがわかります。

参考文献

参考文献

【1】History of Formal Verification at Intel

https://dac.com/blog/post/history-formal-verification-intel

[2] 王建: 正式な検証について話しましょう

http://chainb.com/?P=Cont&id=1957

【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher

https://link.springer.com/chapter/10.1007/11768869_6

【4】Tenth NASA Formal Methods Symposium 

https://shemesh.larc.nasa.gov/NFM2018/

[5] Yutuが使用する国産のSpaceOSオペレーティングシステムは、将来的には民間版に派生すると予想されている

http://blog.sina.com.cn/s/blog_ae55841d0101hemg.html

【6】Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A. and Tchaltsev, A., 2012, July. Formal verification and validation of ERTMS industrial railway train spacing system. In International Conference on Computer Aided Verification (pp. 378-393). Springer, Berlin, Heidelberg.

【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODE https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/

[8] Dirty Cowを使って港湾労働者からの脱出を実現する

https://www.anquanke.com/post/id/84866

【9】CertiKOS: Yale develops world’s first hacker-resistant operating system

https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712

【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16)

【11】THE DAOに対する攻撃手法を技術的観点から分析

https://www.8btc.com/article/93713

【12】kframework/evm-semantics

https://github.com/kframework/evm-semantics

【13】ベンチャーキャピタル大手A16Z、安定通貨プロジェクトMakerDAOに投資

https://www.jinse.com/bitcoin/246582.html

[14] スマートコントラクトのセキュリティ問題を解決するための正式な証明の構築 - 契約を早急に証明する必要がある

https://mp.weixin.qq.com/s/xUNKT8v9ikEYFnuMWzvXdg

【15】Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP '09).