セキュアなスマートコントラクト開発のための形式手法活用（TLA+/Coq入門編）
6.5K Views
May 10, 23
スライド概要
2023年5月10日
DMM.com × CryptoGames勉強会 の発表資料です
https://connpass.com/event/280840/
関連スライド
各ページのテキスト
セキュアなスマートコントラクト開発のための 形式手法活用（TLA+/Coq入門編） 2023-05-10 DMM.com × CryptoGames勉強会 合同会社DMM.com 加嵜 長門
自己紹介 ■ 加嵜 長門 (Kasaki Nagato) 来歴 2014.4 DMM.comグループ 入社 2014.6~2018.4 CTO室/ビッグデータ部 : データ分析基盤システム立ち上げ・レコメンド開発 2018.5~2021.3 スマートコントラクト事業部 /ブロックチェーン研究室 : ブロックチェーン活用事業企画・技術開発 2022.5~ Web3事業部: テックグループリーダー 2023.1~ 株式会社DM2C Studio: CTO 著書 『試して学ぶ スマートコントラクト開発』 (マイナビ出版 ) 『ブロックチェーンアプリケーション開発の教科書』 (マイナビ出版 ) 『ビッグデータ分析・活用のための SQLレシピ』(マイナビ出版 ) 『詳解Apache Spark』(技術評論社)
DMMグループでの形式手法勉強会 TLA＋勉強会 ● 2021年10月～2022年11月 マルレクの丸山先生を招いて、 TLA+のハンズオンセミナーを月１回程度で開催 参考: マルレク / AWSでの形式手法の利用 https://www.marulabo.net/docs/aws-formal/ Coq勉強会 ● 2023年1月～ TLA+に引き続き、Coqのハンズオンセミナーを月１回程度で開催中 参考: マルレク / はじめてのCoq https://www.marulabo.net/video/coq/
Table of Contents 1. 形式手法とはなにか 形式手法にまつわる概念の解説と 形式手法のメリット紹介 3. 形式手法を学ぶ モチベーション なぜ形式手法を学ぶのか 2. ブロックチェーンと 形式手法 4. TLA+, Coq入門 ブロックチェーンにおける 形式手法の活用例 注目している形式手法（TLA+, Coq）の学び方
形式手法とはなにか 形式手法にまつわる概念の解説と 形式手法のメリット紹介
形式手法とは 形式手法 (Formal Methods) ● 数理論理学に基づく言語やツール群 、および、それらを使った ソフトウェア開発手法 数理論理学: 述語論理（Predicate logic）、時相論理（ Temporal Logic）、ホーア論理（ Hoare logic）など 言語・ツール群 : Coq, TLA+, Alloy, VDM, Z言語, … 形式仕様 (Formal Specification) ● 形式手法を用いて、 システムの仕様を厳密に記述 すること 形式検証 (Formal Verification) ● 形式手法を用いて、 システムの「正しさ」を検証 すること
仕様の記述 理想の仕様 記述された仕様 自然言語 UML等 形式手法 仕様書 あいまい 機械が理解しにくい 図式 形式仕様 厳密 機械が理解しやすい
TLA+を用いた形式仕様の例 ① C言語によるプログラム ② 数学表現による仕様記述 ③ TLA+による仕様記述 https://lamport.azurewebsites.net/video/video2-script.pdf
形式手法のメリット ● 厳密な言語を用いることで 仕様を明確化 できる ● 仕様に不備や矛盾がないことを 数学的に証明 し品質を保証できる ● 仕様に含まれている隠れた 不具合を早期（実装・テスト前）に発見 できる ● 正しいシステム だけを系統的に開発できる ソフトウェア工学の道具としての形式手法 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf
身近な形式検証 型システム ● ● ● 軽量（Light-Weight）な形式検証 メリット 型定義が簡易的な仕様書として扱える プログラムの実行・テスト実装前に、型エラーを検出できる 例: JavascriptとTypeScript AirbnbはTypeScriptによって38%のバグを防止 https://www.youtube.com/watch?v=P-J9Eg7hJwE&t=714s function sum (a, b) { return a + b } function sum(a: number, b: number): number { return a + b }
ブロックチェーンと形式手法 ブロックチェーンにおける 形式手法の活用例
ブロックチェーンでの活用 ● ● ● ● Ethereum Formal Verification https://github.com/leonardoalt/ethereum_formal_verification_overview Formal Verification: Tezos’s Feature Nobody Talks About https://tezos.org.ua/en/blog/formal-verification Pact Formal Verification: Making Blockchain Smart Contracts Safer https://medium.com/kadena-io/pact-formal-verification-for-blockchain-smart-contracts-don e-right-889058bd8c3f The DAOハックや、Parityのマルチシグウォレットハック、ウォレット凍結問題など、スマートコントラク トのセキュリティ上の欠陥が原因で盗まれたり失われたりした価値の総額は 10億ドルを超えると推定 される https://ethereum.org/ja/developers/docs/smart-contracts/security/
Formal verification Spectrum Unit testing ● ● ● 仕様を正しく実装しているか？を、特定の入力値と期待出力からテスト ブラックボックステスト、ホワイトボックステスト、経験ベーステストなど 今回の発表スコープではないが、ユニットテストも重要 詳しく知りたい人は … https://sqripts.com/ https://medium.com/kadena-io/pact-formal-verification-for-blockchain-smart-contracts-done-right-889058bd8c3f
Formal verification Spectrum Quickcheck ● ● ● 多量のテストデータを（半）自動的に生成するテスト手法 fuzzing / fuzz testingなど Ethereum では Foundry が対応している https://book.getfoundry.sh/forge/fuzz-testing https://medium.com/kadena-io/pact-formal-verification-for-blockchain-smart-contracts-done-right-889058bd8c3f
Formal verification Spectrum Pact FV ● ● ● Kadenaブロックチェーンの Pact言語における形式検証 プログラム中に記載したアノテーションをもとに静的コード解析 詳しくは過去発表資料を参照 … https://www.slideshare.net/knagato/pact-language Ethereumにおける静的コード解析例 Slither (https://github.com/crytic/slither): 過去の脆弱性事例をもとにした Solidityの静的解析 Mythril (https://github.com/ConsenSys/mythril): EVMバイトコードの静的解析
Formal verification Spectrum Full Specification ● ● ● TLA+やCoqを使った形式仕様はこちら 左から右にいくほど、数学的な保証の度合いは強い すべてをFull Specificationで記述するのは現実的ではなく、さまざまなテスト・検証手法を組み合わ せて活用することが必要
形式手法を学ぶモチベーション なぜ形式手法を学ぶのか
スマートコントラクトのセキュリティ対策 スマートコントラクトは一度デプロイすると変更が難しく、バグの影響度も大きい さまざまな対策があり得るが、どれも万能ではない ● ● ● ● テストを充実させる → すべての脆弱性を事前に検知できるわけではない → 仕様の矛盾や不具合には対応しにくい 第三者によるセキュリティ監査をおこなう → 費用や時間がかかり、継続的な開発には向かない できるだけ監査済のコードやライブラリを使う → 柔軟な開発ができない → ライブラリも脆弱性がゼロというわけではない 盗難・紛失に備えた保険を活用する → 保険料・補償額のトレードオフ
Don’t Trust. Verify. ● ● ● 著名なライブラリや監査済コードも、脆弱性ゼロを保証するわけではない 最終的には使用者の自己責任 OpenZeppelinのライブラリで出会った脆弱性 ■ Double spend exploit https://github.com/OpenZeppelin/openzeppelin-contracts/blob/release-v4.8/contracts/token/ERC20/IERC20.sol#L57 ■ Access Control Deadlock https://github.com/OpenZeppelin/openzeppelin-contracts/blob/release-v4.8/contracts/access/AccessControl.sol#L163 ■ Zero Division Error https://github.com/OpenZeppelin/openzeppelin-contracts/blob/release-v4.8/contracts/finance/VestingWallet.sol#L146 ● 必要なのは、信頼ではなく、数学的事実に基づき誰もが検証可能な証明
- https://github.com/OpenZeppelin/openzeppelin-contracts/blob/release-v4.8/contracts/token/ERC20/IERC20.sol#L57
- https://github.com/OpenZeppelin/openzeppelin-contracts/blob/release-v4.8/contracts/access/AccessControl.sol#L163
- https://github.com/OpenZeppelin/openzeppelin-contracts/blob/release-v4.8/contracts/finance/VestingWallet.sol#L146
仕様の変化に対応する ● Web3サービスは、コントラクト部分のロジックが普遍だとしても、オフチェーン部分の追加開発や 仕様変更などは頻繁に発生しうる ● 特にGameFiやDeFiサービスなどでは、システムのバランスを崩壊させるような追加仕様が致命 的なリスクとなる ユーザーの利益を損なうような修正（アイテムのナーフなど）も受け入れられにくい ● 形式手法による形式仕様を導入することで、仕様の明確化や、仕様の不具合チェック、既存仕様 と追加仕様との整合性チェックなどが容易になる
仕様の変化に対応する ● 引用: DeNA TechCon 2020「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」 https://swet.dena.com/entry/2020/03/17/165835
仕様の変化に対応する ● 引用: DeNA TechCon 2020「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」 https://swet.dena.com/entry/2020/03/17/165835
ブロックチェーンを理解するためのツール TLA+との出会い ● TLA+はLeslie Lamport先生によって開発された形式仕様言語 ● Fast Paxosという論文の中で、 TLA+によるSpecificationがおこなわれている https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-112.pdf Leslie Lamport ● 分散コンピューティングシステムの研究者 ● 2013年 チューリング賞受賞 ● 論理クロック・ビザンチン将軍問題・ Paxosアルゴリズム・ラン ポート署名など、分散システムやブロックチェーンを理解する 上で重要となる概念・アルゴリズムの発明者 ● LaTeXの開発者でもある https://commons.wikimedia.org/wiki/File:Leslie_Lamport.jpg
人工知能の歴史の１歩先を見据えて 統計・確率系 1960年代 集合・論理系 第一次人工知能 ブーム ● ● ニューラルネットワーク 遺伝アルゴリズム ● ● 探索、推論 エキスパートシステム 第二次人工知能 ブーム ● ● 統計的自然言語処理 音声認識 ● ● 知識ベース 自動推論 ディープラーニング Diffusionモデル LLM / GPT ● ？？？ 第三次人工知能 ブーム ● ● ● 1980年代 2000年代 2020年代 情報通信白書 https://www.soumu.go.jp/johotsusintokei/whitepaper/ja/h28/html/nc142120.html
TLA+, Coq入門 注目している形式手法（TLA+, Coq） の学び方
TLA+ ● ● インストール 公式ページから、 TLA+ Toolboxをダウンロード https://lamport.azurewebsites.net/tla/toolbox.html Visual Studio Codeのエクステンションもある https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus 学習方法 Lamport先生によるビデオコース https://lamport.azurewebsites.net/video/videos.html 英語が聞き取りやすく、説明も丁寧 後半からは難易度が高い（分散システムのアルゴリズムの理解が必要） 書籍 Specifying Systems https://lamport.azurewebsites.net/tla/book.html
Coq ● ● ● インストール 公式サイト https://coq.inria.fr/download 開発環境 Coq Jupyter https://github.com/maruyama097/coq-tutorial 学習用には使いやすい CoqIDE / Emacs / Visual Studio Code プロジェクトを開発するには、 IDEが便利 学習方法 ソフトウェアの基礎 http://proofcafe.org/sf/ Coqを用いた、ソフトウェア工学のための論理学入門
TLA+ & Coq の活用計画 ● TLA+ 複数の異なるシステムが協調して動作する仕様の記述・検証に使いたい 例: クロスチェーンブリッジ、オンチェーンとオフチェーンの連携機能 ● Coq セキュリティが重要となるプロダクト開発プロセスに組み込みたい 初期は、比較的小規模の単一プロダクトで検証してみる 例: スマートコントラクト、オンラインウォレットシステムの仕様記述 ● ● 成果物については今後の発表をお待ちください Web3サービスの形式手法プロセスや、 DMMのWeb3への取り組みに興味がある方は、お気軽にお 声がけください
Thanks! 質問・ご意見など [email protected] CREDITS: This presentation template was created by Slidesgo, including icons by Flaticon, and infographics & images by Freepik. Please keep this slide for attribution.