---
title: セキュアなスマートコントラクト開発のための形式手法活用（TLA+/Coq入門編）
tags: 
author: [加嵜 長門](https://convert.docswell.com/user/knagato)
site: [Docswell](https://www.docswell.com/)
thumbnail: https://bcdn.docswell.com/page/2EVLW3KNJQ.jpg?width=480
description: 2023年5月10日 DMM.com × CryptoGames勉強会 の発表資料です https://connpass.com/event/280840/
published: May 10, 23
canonical: https://convert.docswell.com/s/knagato/598GRM-2023-05-10
---
# Page. 1

![Page Image](https://bcdn.docswell.com/page/2EVLW3KNJQ.jpg)

セキュアなスマートコントラクト開発のための
形式手法活用（TLA+/Coq入門編）
2023-05-10
DMM.com × CryptoGames勉強会
合同会社DMM.com 加嵜 長門


# Page. 2

![Page Image](https://bcdn.docswell.com/page/57GXD3Q5EL.jpg)

自己紹介
■ 加嵜 長門 (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』(技術評論社)


# Page. 3

![Page Image](https://bcdn.docswell.com/page/4EQ815KLJP.jpg)

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/


# Page. 4

![Page Image](https://bcdn.docswell.com/page/KJ42R9P5E1.jpg)

Table of Contents
1. 形式手法とはなにか
形式手法にまつわる概念の解説と
形式手法のメリット紹介
3. 形式手法を学ぶ
モチベーション
なぜ形式手法を学ぶのか
2. ブロックチェーンと
形式手法
4. TLA+, Coq入門
ブロックチェーンにおける
形式手法の活用例
注目している形式手法（TLA+,
Coq）の学び方


# Page. 5

![Page Image](https://bcdn.docswell.com/page/LE1MQK927G.jpg)

形式手法とはなにか
形式手法にまつわる概念の解説と
形式手法のメリット紹介


# Page. 6

![Page Image](https://bcdn.docswell.com/page/GEW3MDQ2E2.jpg)

形式手法とは
形式手法 (Formal Methods)
●
数理論理学に基づく言語やツール群 、および、それらを使った ソフトウェア開発手法
数理論理学: 述語論理（Predicate logic）、時相論理（ Temporal Logic）、ホーア論理（ Hoare
logic）など
言語・ツール群 : Coq, TLA+, Alloy, VDM, Z言語, …
形式仕様 (Formal Speciﬁcation)
●
形式手法を用いて、 システムの仕様を厳密に記述 すること
形式検証 (Formal Veriﬁcation)
●
形式手法を用いて、 システムの「正しさ」を検証 すること


# Page. 7

![Page Image](https://bcdn.docswell.com/page/47ZVQGW4E3.jpg)

仕様の記述
理想の仕様
記述された仕様
自然言語
UML等
形式手法
仕様書
あいまい
機械が理解しにくい
図式
形式仕様
厳密
機械が理解しやすい


# Page. 8

![Page Image](https://bcdn.docswell.com/page/YJ656YGG7V.jpg)

TLA+を用いた形式仕様の例
① C言語によるプログラム
② 数学表現による仕様記述
③ TLA+による仕様記述
https://lamport.azurewebsites.net/video/video2-script.pdf


# Page. 9

![Page Image](https://bcdn.docswell.com/page/GJ5Y6GVXJ4.jpg)

形式手法のメリット
●
厳密な言語を用いることで 仕様を明確化 できる
●
仕様に不備や矛盾がないことを 数学的に証明 し品質を保証できる
●
仕様に含まれている隠れた 不具合を早期（実装・テスト前）に発見 できる
●
正しいシステム だけを系統的に開発できる
ソフトウェア工学の道具としての形式手法 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf


# Page. 10

![Page Image](https://bcdn.docswell.com/page/9E2GMY3QER.jpg)

身近な形式検証
型システム
●
●
●
軽量（Light-Weight）な形式検証
メリット
型定義が簡易的な仕様書として扱える
プログラムの実行・テスト実装前に、型エラーを検出できる
例: JavascriptとTypeScript
AirbnbはTypeScriptによって38%のバグを防止
https://www.youtube.com/watch?v=P-J9Eg7hJwE&amp;t=714s
function sum (a, b) {
return a + b
}
function sum(a: number, b: number): number {
return a + b
}


# Page. 11

![Page Image](https://bcdn.docswell.com/page/D7YVXG1Y7M.jpg)

ブロックチェーンと形式手法
ブロックチェーンにおける
形式手法の活用例


# Page. 12

![Page Image](https://bcdn.docswell.com/page/VENM1G2RJ8.jpg)

ブロックチェーンでの活用
●
●
●
●
Ethereum Formal Veriﬁcation
https://github.com/leonardoalt/ethereum_formal_veriﬁcation_overview
Formal Veriﬁcation: Tezos’s Feature Nobody Talks About
https://tezos.org.ua/en/blog/formal-veriﬁcation
Pact Formal Veriﬁcation: Making Blockchain Smart Contracts Safer
https://medium.com/kadena-io/pact-formal-veriﬁcation-for-blockchain-smart-contracts-don
e-right-889058bd8c3f
The DAOハックや、Parityのマルチシグウォレットハック、ウォレット凍結問題など、スマートコントラク
トのセキュリティ上の欠陥が原因で盗まれたり失われたりした価値の総額は 10億ドルを超えると推定
される
https://ethereum.org/ja/developers/docs/smart-contracts/security/


# Page. 13

![Page Image](https://bcdn.docswell.com/page/Y79N5W1Z73.jpg)

Formal veriﬁcation Spectrum
Unit testing
●
●
●
仕様を正しく実装しているか？を、特定の入力値と期待出力からテスト
ブラックボックステスト、ホワイトボックステスト、経験ベーステストなど
今回の発表スコープではないが、ユニットテストも重要
詳しく知りたい人は … https://sqripts.com/
https://medium.com/kadena-io/pact-formal-verification-for-blockchain-smart-contracts-done-right-889058bd8c3f


# Page. 14

![Page Image](https://bcdn.docswell.com/page/G78KYN3YJD.jpg)

Formal veriﬁcation 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


# Page. 15

![Page Image](https://bcdn.docswell.com/page/L7LZ4PV9ER.jpg)

Formal veriﬁcation 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バイトコードの静的解析


# Page. 16

![Page Image](https://bcdn.docswell.com/page/4EMVK4GVEW.jpg)

Formal veriﬁcation Spectrum
Full Speciﬁcation
●
●
●
TLA+やCoqを使った形式仕様はこちら
左から右にいくほど、数学的な保証の度合いは強い
すべてをFull Speciﬁcationで記述するのは現実的ではなく、さまざまなテスト・検証手法を組み合わ
せて活用することが必要


# Page. 17

![Page Image](https://bcdn.docswell.com/page/PER2XWZW79.jpg)

形式手法を学ぶモチベーション
なぜ形式手法を学ぶのか


# Page. 18

![Page Image](https://bcdn.docswell.com/page/P7XD6P9VJX.jpg)

スマートコントラクトのセキュリティ対策
スマートコントラクトは一度デプロイすると変更が難しく、バグの影響度も大きい
さまざまな対策があり得るが、どれも万能ではない
●
●
●
●
テストを充実させる
→ すべての脆弱性を事前に検知できるわけではない
→ 仕様の矛盾や不具合には対応しにくい
第三者によるセキュリティ監査をおこなう
→ 費用や時間がかかり、継続的な開発には向かない
できるだけ監査済のコードやライブラリを使う
→ 柔軟な開発ができない
→ ライブラリも脆弱性がゼロというわけではない
盗難・紛失に備えた保険を活用する
→ 保険料・補償額のトレードオフ


# Page. 19

![Page Image](https://bcdn.docswell.com/page/37KX1DP5JD.jpg)

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/ﬁnance/VestingWallet.sol#L146
●
必要なのは、信頼ではなく、数学的事実に基づき誰もが検証可能な証明


# Page. 20

![Page Image](https://bcdn.docswell.com/page/LJ35QRX175.jpg)

仕様の変化に対応する
●
Web3サービスは、コントラクト部分のロジックが普遍だとしても、オフチェーン部分の追加開発や
仕様変更などは頻繁に発生しうる
●
特にGameFiやDeFiサービスなどでは、システムのバランスを崩壊させるような追加仕様が致命
的なリスクとなる
ユーザーの利益を損なうような修正（アイテムのナーフなど）も受け入れられにくい
●
形式手法による形式仕様を導入することで、仕様の明確化や、仕様の不具合チェック、既存仕様
と追加仕様との整合性チェックなどが容易になる


# Page. 21

![Page Image](https://bcdn.docswell.com/page/8JDD9Y2KJG.jpg)

仕様の変化に対応する
●
引用: DeNA TechCon 2020「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」
https://swet.dena.com/entry/2020/03/17/165835


# Page. 22

![Page Image](https://bcdn.docswell.com/page/VEPXZ613J8.jpg)

仕様の変化に対応する
●
引用: DeNA TechCon 2020「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」
https://swet.dena.com/entry/2020/03/17/165835


# Page. 23

![Page Image](https://bcdn.docswell.com/page/27VLW3YNEQ.jpg)

ブロックチェーンを理解するためのツール
TLA+との出会い
● TLA+はLeslie Lamport先生によって開発された形式仕様言語
● Fast Paxosという論文の中で、 TLA+によるSpeciﬁcationがおこなわれている
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


# Page. 24

![Page Image](https://bcdn.docswell.com/page/5JGXD3957L.jpg)

人工知能の歴史の１歩先を見据えて
統計・確率系
1960年代
集合・論理系
第一次人工知能
ブーム
●
●
ニューラルネットワーク
遺伝アルゴリズム
●
●
探索、推論
エキスパートシステム
第二次人工知能
ブーム
●
●
統計的自然言語処理
音声認識
●
●
知識ベース
自動推論
ディープラーニング
Diffusionモデル
LLM / GPT
●
？？？
第三次人工知能
ブーム
●
●
●
1980年代
2000年代
2020年代
情報通信白書 https://www.soumu.go.jp/johotsusintokei/whitepaper/ja/h28/html/nc142120.html


# Page. 25

![Page Image](https://bcdn.docswell.com/page/47Q815WLEP.jpg)

TLA+, Coq入門
注目している形式手法（TLA+, Coq）
の学び方


# Page. 26

![Page Image](https://bcdn.docswell.com/page/KE42R9K571.jpg)

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


# Page. 27

![Page Image](https://bcdn.docswell.com/page/L71MQKX2JG.jpg)

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を用いた、ソフトウェア工学のための論理学入門


# Page. 28

![Page Image](https://bcdn.docswell.com/page/G7W3MDN272.jpg)

TLA+ &amp; Coq の活用計画
●
TLA+
複数の異なるシステムが協調して動作する仕様の記述・検証に使いたい
例: クロスチェーンブリッジ、オンチェーンとオフチェーンの連携機能
●
Coq
セキュリティが重要となるプロダクト開発プロセスに組み込みたい
初期は、比較的小規模の単一プロダクトで検証してみる
例: スマートコントラクト、オンラインウォレットシステムの仕様記述
●
●
成果物については今後の発表をお待ちください
Web3サービスの形式手法プロセスや、 DMMのWeb3への取り組みに興味がある方は、お気軽にお
声がけください


# Page. 29

![Page Image](https://bcdn.docswell.com/page/4JZVQG3473.jpg)

Thanks!
質問・ご意見など
kasaki-nagato@dmm.com
CREDITS: This presentation template was created by
Slidesgo, including icons by Flaticon, and infographics &amp;
images by Freepik.
Please keep this slide for attribution.


