日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

SCameleer: スマートコントラクト記述言語 SCamlのための自動検証器
服部 佑哉

西田 雄気

古瀬 淳

末永 幸平

五十嵐 淳

スマートコントラクトのバグは多額の金銭的な損害を生じる可能性があるため，静的かつ形式的に検証して安全性を保証することが望ましい．SCaml は Tezos のためのスマートコントラクトを記述するための OCaml 互換なプログ
ラミング言語である．本論文では SCaml のための自動検証器 SCameleer について述べる．SCameleer は OCamlのための演繹的検証器 Cameleer の拡張として実装されており，仕様を表す注釈を加えた SCaml のコードを受け取り，プログラムが仕様を満たすか否かを自動で判断する．拡張は主に SCaml の基本ライブラリの機能を SCameleerに移植することにより行った．ただし，Cameleer は OCaml のいくつかの機能を制限しているため，非自明な移植が必要な箇所があった．いくつかのスマートコントラクトの例を挙げ，実際にどのような性質が検証可能かを示す．

There is surging demand for a method that can statically and formally verify smart contract since bugs insmart contracts may cause signiﬁcant ﬁnancial damage, t. SCaml is a strict subset of OCaml and is used towrite smart contracts that are executed on the blockchain platform Tezos. This paper describes SCameleer,
an automatic veriﬁer for SCaml. SCameleer is implemented as an extension of Cameleer, a deductive veriﬁer
for OCaml. SCameleer takes an SCaml program annotated with a user-deﬁned speciﬁcation and automatically veriﬁes the program against the speciﬁcation. We extended SCameleer so that it handles types andvalues in the standard library of SCaml. Due to restrictions of Cameleer, some standard library functions
requires nontrivial porting. We show some examples of smart contracts and what properties can be veriﬁed
in practice.

ラムは多くのブロックチェーンでブロックチェーン上

1 はじめにに記録されるアカウントに関連付けられており，アカ

ブロックチェーンは分散型台帳を非中央集権的に，ウントへの送金が起こったタイミングで起動される．

かつ信頼性の高い方法で実現するための仕組みであスマートコントラクトはブロックチェーン上に内部状

り，現在では多くの非中央集権型のアプリケーション

態を保持することができ，この仕組みを用いて契約やの基盤となっている．また，ブロックチェーンは多数取引の自動化をはじめとする，様々なアプリケーショの計算機が合意形成に参加することを前提とした仕ンが実装されている．スマートコントラクト実行機能組みであり，その参加に対するインセンティブとしてを持つブロックチェーンでは，プログラムを動作させ参加者に暗号通貨が配布される．この暗号通貨は金銭るための仮想機械が実装されており，プログラムの実的価値の授受を伴う決済手段として用いられている．

行はこの仮想機械を合意形成の参加者が動作させる

近年のブロックチェーンにはスマートコントラク

ことで行われる．スマートコントラクトの記述には，トと呼ばれるプログラムをブロックチェーン上で動作

Tezos [1] における Michelson [10] のように，それぞさせるための仕組みを備えたものが多い．このプログ

れのブロックチェーンで定義されている仮想機械の命
令列を直接記述する方法や，これらの命令列にコンパ

Yuya Hattori, Yuki Nishida, Kohei Suenaga, Atsushi
Igarashi, 京 都 大 学 大 学 院 情 報 学 研 究 科, Graduate
School of Informatics, Kyoto University.
Jun Furuse, ダイラムダ株式会社, Dailambda Inc..

イルされる高級言語を用いる方法がある．

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

2
1

parameter unit ;2storage unit ;

3

code

4

{ CDR ;

5

NIL operation ;6

AMOUNT ;7

PUSH mutez 0;

8

IFCMPEQ

9

{}

10

{

11

SOURCE ;12

CONTRACT unit ;13

ASSERT_SOME ;14

AMOUNT ;15

UNIT ;

16

TRANSFER_T OK EN S ;

17

CONS

18

} ;

19

PAIR }

図1

boomerang.tz

ブロックチェーンの一種である Tezos には，LIGO†1
や SmartPy†2 等の Michelson にコンパイルされる高器 Cameleer [9] を，SCaml プログラムを扱えるよう

級言語がいくつか開発されている．SCaml†3 はそのサブセットとして実装されているため Cameleer のような言語の一つであり，プログラムは OCaml のサ適用は比較的容易であるが，以下の点で拡張が必要でブセットを用いて記述し，処理系が OCaml と同様のあった．

型検査を行った後に，Michelson にプログラムをコンパイルする．

に拡張したツールである．SCaml 言語は OCaml の• スマートコントラクト記述のために SCaml が提供しているプリミティブの仕様を Cameleer が一方で，スマートコントラクトには，高い金銭的価検証で利用できるように拡張を行った．その際値を持つ暗号通貨を扱うために，そのバグが莫大なに，SCaml のプリミティブには，その動作がプ

金銭的被害に直結する．そのため，スマートコントラ

ログラム実行時のブロックチェーンの状態に依存

クトの安全性を保証するための形式検証が研究されするものがあるため，そのような挙動が正しく表ている [8] [4] [2]．例えば Nishida ら [8] は Michelson

現できるように拡張を行う必要があった．

プログラムのための篩型システムを提案し，この型システムに基づく検証器 Helmholtz†4 を実装している．

• SCaml のプリミティブには GADT を用いて定

また，Coq を用いてスマートコントラクトの動作をは GADT を用いたプログラムを扱うことができモデリングし検証する研究も行われている [4] [2]．

ないため，SCaml のプログラムを手動でシステ

本論文では，Tezos でスマートコントラクトを記述するための言語 SCaml のための形式検証器

義されているものがあるが，Why3 や Cameleer

マティックに GADT を使わないプログラムに変換する方法を与えた．

SCameleer について述べる．SCameleer は Why3 [7]また，実装した SCameleer を用いて SCaml に含まを用いて実装されている OCaml のための形式検証れるいくつかの SCaml プログラムが期待通りに検証

†1
†2
†3
†4

できることを示した．
https://ligolang.org/
https://smartpy.io/
https://scamlang.dev/
https://www.fos.kuis.kyoto-u.ac.jp/projects/
Helmholtz/

本論文の構成は以下のとおりである．2 節で SCaml
について説明を行う．3 節で SCameleer の実装について説明する．4 節でいくつかのスマートコントラク

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

3

トを例に挙げ，実際に SCameleer がどのような性質

SCaml.operation list, ’storage)型を持つ．ここを検証可能であるかを示す．5 節で関連研究を紹介すで Code’parameter はこのスマートコントラクトの引る．最後，6 節で結論と今後の課題について述べる．

数の型を，’storageは内部状態の型を表す．返り値は(1) このスマートコントラクトが実行された後に実行

2 SCaml
SCaml†5 は Tezos のためのスマートコントラクトを記述するための高級言語の一つである．SCaml はされるべき操作の列を表す SCaml.operation list型の値と (2) 更新後の内部状態の値を表す’storage型の値のペアである．

OCaml 互換なプログラミング言語として設計されて4 行目以降は関数 mainの定義である．4 行目ではおり，プログラムを Michelson に変換するコンパイ

Global.get_amount関数を用いて，このスマートコラとして実装されている．OCaml のプリミティブやントラクトに送金された金額を取得している．5–11

標準ライブラリに加えて，スマートコントラクトを記行目で，mainによって発行される操作列を表現する

述するためのプリミティブがライブラリとして提供さ

SCaml.operation list型の値を計算して，変数 ops

れている．

をその値に束縛している．送金額が 0 であれば (6 行

図 2 に SCaml プログラムの例を示す．この例は前目) 操作は行わないため，操作列は []となる．そう

述した boomerang に相当する SCaml プログラムででない場合は，送金された金額を取引を開始したアカある．一般にスマートコントラクトは，プログラムがウントに返金するために，返金を行うための操作を作関連付けられたアカウントに送金が行われることで成する．9 行目は取引を開始したアカウントを計算す起動されるが，boomerang は送金された金額をそのる式である．この式では以下の計算を行っている．

まま取引を開始したアカウントに送り返すプログラ• Global.get_source ()で取引を開始したアカムである．

ウントのアドレスを取得している．

以下では図 2 のプログラムを説明する．1 行目では

• このアドレスを Contract.contract関数に引数モジュール SCamlが open されている．このモジューとして与えている．この関数はアカウントのアド

ルは SCaml が提供するスマートコントラクト記述用

レスを引数として受け取り，そのアドレスが関連のプリミティブを提供するモジュールである．このモ付けられているスマートコントラクトが要求されジュールには，以下で使用する Tz等のコンストラク

る型を持つかを検査する関数である．以下で述べ

タや，Globalや Contract等のモジュールの定義が含る通り，関数 mainは返金操作において ()を引数まれている．

として返金先に与えるため，返金先が unit型を

SCaml においてスマートコントラクトにコンパイ引数として受け取るスマートコントラクトであルされるべき関数の定義には@entry属性が付加されることを要求している．Contract.contractはる．図 2 では main関数の定義にこの属性が付加されGlobal.get_source ()が返すアドレスに関連ている．
一般に Tezos のスマートコントラクトは内部状態付けられたコントラクトがこの通りの型を持つかを検査する関数である．†6 この関数は，型検(storage) を持ち引数 (parameter) を一つ取り，実査の成否を contract option型の値として返す．

行されると内部状態を更新する．また，スマートコ

contract型は型検査が成功したスマートコント

ントラクトは実行後にブロックチェーン上で送金やラクトを表す値である．型検査が成功したならばアカウント作成等の操作 (operation) を行うことがこの値 cを Some cとして返し，失敗したならばできる．これに対応して，SCaml において@entry

Noneとして返す．

が付加された関数は’parameter -> ’storage -> (†5 https://scamlang.dev/†6 Tezos のスマートコントラクトはすべて静的型を持
つように設計されている．

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

4
1

open SCaml23let [@entry] main ( ) ( ) =4

let amount = G lo bal .g e t_ am o unt ( ) in5

let ops =6

if amount = Tz 0. then []

7

else

8

let source_contract =9

Option.get @@ C ont ra c t. con tra ct @@ G lo b a l. get _s ou r c e ( ) in10

[ O p e r a t i o n . t r a n s f e r _ t o k e n s ( ) amount so u rc e_contract ]

11

in

12

ops, ( )図2boomerang.ml• Contract.contractの結果を Option.getに渡す．Option.getは 引 数 が Some cな ら ば cを 返!"#$%&'&(!)*+,

し，Noneならば例外を発生させる．

10 行目ではこの計算から操作列を計算している．

=#>72$#745&79#?@%#742?&A/&"#$B%BB9C

Operation.transfer_tokensは送金を表す操作を作成する関数であり，第 1 引数に送金先にわたす引-./0,

数（ここでは ()）を，第 2 引数に送金額（ここでは-./1&%2345

amount）を，第 3 引数に送金先のコントラクトを表す contract型の値を受け取る．上記の計算を行った上で，関数 mainの返り値のペアを 12 行目で計算し<1

6%78+932":";ている．第 1 要素の操作列は 10 行目で計算した操作列である．内部状態は ()のまま変化しないので，ペ

図3Cameleer の処理の流れ

アの第 2 要素は ()である．
バや証明支援系と容易に接続できるようになってお3 SCameleer

り，これらを用いて検証条件が成り立つかどうかを本研究では SCaml のための検証器 SCameleer をチェックすることが可能となっている．所望のプログ実装した．実装にあたっては OCaml のための検証器

ラミング言語から WhyML への変換を Why3 のプ

Cameleer [9] をベースとした．本節ではまず Cameleer

ラグインとして実装することができ，この機能を用いが実装に用いているフレームワーク Why3 [7] についることで様々な言語のための形式検証器を低いコストて説明した後に，Cameleer と SCameleer の実装にで実装することができる．

ついて説明する．

3. 2 Cameleer
3. 1 Why3

Cameleer [9] は，OCaml のための演繹的なプログ

検証器は Why3 フレームワーク [7] を用いて実装

ラム検証ツールである．Cameleer は GOSPEL といされている．Why3 フレームワークは演繹的検証器

う仕様記述言語を用いて仕様を注釈した OCaml のを実装するためのフレームワークであり，プログラ

プログラムを受け取り，プログラムが仕様を満たす

ムと仕様を記述するための関数型言語 WhyML と，かどうかを検証する．GOSPEL による仕様記述では

WhyML プログラムを検証するための検証条件生成

OCaml のサブセットと一階述語論理と分離論理の拡器とが提供されている．Why3 は様々な SMT ソル

張を用いることができる．

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

5

Cameleer の実装には Why3 が用いられており，• ブロックチェーンの状態に依存する動作のエン注釈された OCaml プログラムから WhyML へのコーディング: SCamlモジュールが提供する関変換がプラグインとして提供されている．図 3 に

数には，その動作がスマートコントラクトが呼Cameleeer の処理の流れを示す．Why3 の機能を用び出された時点でのブロックチェーンの状態にいて，Alt-Ergo [5] や CVC4 [3]，Z3 [6] などの SMT依存するものがある．例えば，上述したようにソルバを用いた検証条件のチェックが可能となってSCaml.contract 関数はアドレスに関連付けらいる．

れているプログラムが期待する通りの型を持つ

また，Cameleer は OCaml の標準ライブラリを用かどうかを検査する．この動作はブロックチェー

いたプログラムも検証できるように，標準ライブラリ

ン上でアドレスに関連付けられているプログラのインターフェイスを WhyML に移植している．具体

ムに依存するため，Cameleer で検証する際には，的には ocamlstdlib.mlw というファイルに OCaml

型検査が成功する場合と失敗する場合の両方がの標準ライブラリの一部のインターフェイスとその仕起こり得ることを想定して SCaml.contract関数

様に加えて，検証を行う上で有用な補題がいくつか

WhyML 言語で記述されている．

の動作をエンコードしなければならない．
これらのギャップのうち 1 つ目の点については，Cameleer は OCaml のすべての言語機能をサポー

Cameleer の実装のうち OCaml の標準ライブラリのトしているわけではなく，オブジェクトや GADT，仕様を記述しているファイルである ocamlstdlib.

多相 variant などはサポートされていない．また，高mlw に，WhyML 言語を用いて SCaml モジュールの階関数や mutability などは制限付きでサポートされインターフェイスと仕様を追加することにより対応している．

た．以下においては 2 つ目と 3 つ目の点に対する対処について述べる．

3. 3 SCameleer の実装
SCaml は OCaml 互換なプログラミング言語であるため，Cameleer を利用することで同様に検証を

3. 4 WhyML における GADT のエンコーディ
ング行うことが可能であると期待される．しかしながら，

GADT は通常の代数的データ型の拡張である．

Cameleer が扱える OCaml のサブセットと，SCaml

OCaml の GADT を用いると，多相的な代数的デーとの間には，現在以下のギャップが存在する．

タ型を定義する際に，コンストラクタによって型パラ• SCamlモジュール: SCaml プログラムを記述する際には SCamlモジュールが提供する関数を標メータを変化させることができ，また存在型を伴う
データ型を定義することができる．

準ライブラリと同様に使用する．したがって，

図 4 は SCamlモ ジュー ル の う ち ，contract型 とCameleer で SCaml モジュールの提供する型やoperation型，Contractモジュールの定義に関する値を利用するプログラムを検証するには，それらコードの一部である．型検査された引数として’aの仕様を記述する必要がある．

型の値をとるスマートコントラクトを表現する’a• GADT: SCaml においては ’a operation 型とcontract型の定義において，Implicit_accountコ

operation 型の実装において GADT が用いら

ンストラクタの型が key_hash -> unit contractとれている．しかし Cameleer とその基盤であるなっており，戻り値において型パラメタ’aが unitに

Why3 は GADT をサポートしていない．した

具体化されているので，この型は GADT である．

がって，Cameleer を用いて SCaml プログラム

また，操作を表す operation型の定義においても，を検証するためには，GADT を用いるプログラ

Trasnsfer_tokensコンストラクタの型において，存ムを GADT を用いないプログラムでエンコード

在型のパラメタ’aが使われているので，この型もする必要がある．

GADT である．

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

6
1

type ’a contract =2| Self : ’a contract3| Of_address : address -> ’a contract

4| Implicit_account : key_hash -> unit contract

5
6

type operation =7| Transfer_to ke ns : ’a * tz * ’a contract -> operation

8

...

9
10

type operations = operation list

11
12

module Contract : sig

13

type ’a t = ’a contract

14

val contract : address -> ’a t option

15
16

...
end = struct17

type ’a t = ’a contract18

let contract a = Some (Of_address a )

19
20

...
end

図4

contract モジュール（SCaml）

これらの型を用いるプログラムを WhyML でエることが検査されたコントラクトを表す．

ンコードしたものが図 5 である．エンコードの際にまた，13 行目が operation型の定義である．SCaml

GADT を用いて実装されている型は，(1) 多相的なでは存在型を持つコンストラクタとして定義されて型パラメタが具体化されているコンストラクタに，どいた Transfer_tokensが，param型の値を保持するの型に具体化されたかを表す値を保持させ，(2) 存在

コンストラクタとして定義されている．param型の値型が用いられているコンストラクタに，その型を持

v_param, 通貨量を表す tz型の値 v_tz, contract型

つ値を保持させた．(1) の実装のために，「型を表現すの値 v_contrについて，Transfer_tokens(v_paramる値」の型である repを 1–4 行目において定義した．

,v_tz,v_contr)でスマートコントラクト vcontr を持RepIntと RepUnitはそれぞれ intと unitを表す値でつアカウントに，通貨量 vtz を，vparam が表現する値

あり，RepPair(^@$\tau_1$@^,^@$\tau_2$@^)は τ1を引数として送金する操作を表す．

型と τ2 型のペア型を表す値である．また，(2) の実装のために，「存在型を持つ値の表現としてコンストラク
タに渡す値」の型である paramを 6–9 行目で定義し3. 5 コントラクトに対する型検査の挙動のエン
コーディング

た．ParamInt ^@$n$@^と RepUnitはそれぞれ整数 n

上記の 3 つ目の問題に対処するために，18–19 行目と unit 値の表現，ParamPair(^@$v_1$@^,^@$v_2$@の Contract.contract関数を，型検査が成功する場^)は (^@$v_1$@^,^@$v_2$@^)の表現である．

合と失敗する場合の両方の挙動を表現するように実装

そ の 上 で 11 行 目 に contract の 型 を 定 義 し た ．

した．Contract.contract関数はアドレスを表す値

SCaml の contract型 に は 複 数 の コ ン ス ト ラ ク タ

addrに加えて，型検査において期待される引数の型をが定義されているが，現在の WhyML コードにはrepの値として渡す必要がある．オリジナルの SCaml

Contractというコンストラクタのみが定義されておでは，期待される引数の型は OCaml の型推論機能

り，τ 型を表す rep型の値 v_repとアドレスを表す値を用いて自動的に推論されていたが，SCameleer に

v_addrについて，Contract(v_addr,v_rep)でアド

おいては現在この値を人手で与える必要がある．そのレス v_addrに関連付けられた，τ 型の引数を受け取上で，19 行目では，非決定的に trueまたは falseを

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集
1

type rep =2| RepInt3| RepUnit

4| RepPair (rep, rep )7

5
6

type param =7| ParamInt int

8| ParamUnit

9| ParamPair (param, param )10
11

type contract = Contract (address, rep )12
13

type operation = Transfer_tokens param tz contract

14

type operations = list operation

15
16

scope Contract

17

type t = contract18

let function contract (addr : address ) (r : rep ) : option contract =19
20

if any bool then Some (Contract (addr, r ) ) else None
end

21
22

scope Operation

23

type t = operation24

let function transfer_tokens (p : param ) (t : tz ) (c : contract ) : operation25

requires26{ match c with| Contract (_, r ) ->27

match type_of p with28

| r -> true29

| _ -> false

30

end

31

| _ -> false

32
33
34

end }
= Transfer _tokens p t cend

図5contract モジュール（SCameleer）

返す WhyML の式 any boolを用いてコントラクトの型検査の成否が非決定的に決まる挙動を表現し，成功した場合には Some (Contract(addr,r))を返している．
また，GADT を上記のようにエンコードしたことに4 スマートコントラクトの検証例
本章では SCameleer で検証可能なスマートコント
ラクトの例を挙げ，どのような性質が検証可能であるかを示す．

より，送金操作を表す operation型の値を作成する関
数 transfer_tokensの事前条件に型の整合性に関す

4. 1 Boomerang の検証例

る条件が追加されている．25–32 行目の requires節

図 6 に SCameleer により検証可能な boomerangが transfer_tokensの事前条件を表現した箇所であプログラムを示す．これは図 2 の boomerang プログる．ここではこの関数に渡されている param型の引数

ラムに GOSPEL で仕様を表す注釈をつけたものであpと，contract型の値 cが保持する rep型の値とが整る．10 行目以降の (*@ ...

合していることを要求している．

仕様部分である．10 行目は main 関数の引数と返り) が GOSPEL による値をそれぞれ変数と対応付けている．ここで対応付
けた変数は仕様の記述で使用することができる．続日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

81

let [@entry] main env (param : unit ) (storage : unit ) =2

let amount = G lo bal .g e t_ am o unt env in3

let ops =4

if Tz.eq amount (Tz 0 ) then []

5

else

6

let source_contract = Option.get ( Co n tr a c t . c o n tr a ct ( Gl o ba l .g e t_ s ou r ce env ) ParamUnit ) in7

[ O p e r a t i o n . t r a n s f e r _ t o k e n s ParamUnit amount s ou rce_contr act ]

8
9
10
11
12

in
ops, ( )( * @ ops, stg = main env param storage
ensuresif Tz.eq (G lo b al . ge t _a m ou n t env ) (Tz 0 ) then ops = []
else

13

match Co n tra ct. con tra ct (G l o b a l . g et _ so u r c e env ) ParamUnit with

14

| Some sc -> ops = ( O p e r a t i o n . t r a n s f e r _ t o k e n s ParamUnit (G lo b al . ge t _a m ou n t env ) sc ) :: []15| None -> false

16

raises Inv al id _a rg um en t _ ->17match (C on t ra c t. c on t ra c t (G lo b al . ge t _s o ur c e env ) ParamUnit ) with None -> true | Some _ -> false *)図6boomerang.ml(注釈付き)

く 11 行目の ensures 節で事後条件を記述する．ここの定義である．main 関数は [@entry] が使用されてでは ops の値に関する条件を記述している．このプ

おり，スマートコントラクトとして呼び出すことが可

ログラムが関連づけられたアカウントに送金された能である．7 行目の match 文で処理が分岐している．

金額が 0 の場合，ops が [] であることを保証する．

Left の場合はコントラクトに送金されるだけなので，一方そうでない場合，13 行目の match 文で，取引を空のオペレーションのリストを返す．一方 Right の場開始したアカウントのアドレス Global.get source

合の処理は少し複雑である．まず 10 行目 Address.eq

env を Unit 型のコントラクトへ変換した結果によっ

で，コントラクトを開始したアカウントのアドレスがて処理が分岐する．その変換が成功した場合，14 行

ストレージに保存されているアドレスと一致するかを目にある通り，ops はそのコントラクトに送金され確かめる．一致した場合，Right で指定した金額だけた金額の分だけ金銭を送るオペレーションと一致す

そのアカウントに送金するオペレーションを返す．そることを保証する．一方失敗した場合，true とある

うでければ，不正な取引だと判断しコントラクトは失が，これは例外を表したものである．続く 16 行目

敗する．17 行目以降は仕様を GOSPEL で記述したもの ensures 節は例外事後条件を記述する．ここではのである．まず，17 行目では main 関数の引数を env，

Invarid argument が起こった際，現在の取引を開始

parameter，storage，返り値を ops，stg と対応付したアカウントのアドレス Global.get source env

けている．18 行目の ensures 節で事後条件を記述しの Unit 型のコントラクトへの変換が失敗しており，ている．match 文では parameter と現在の内部取引を結果が None であることを保証している．

開始したアカウントのアドレス Global.get sender

env を Unit 型のコントラクトに変換した結果によっ
4. 2 deposit プログラムの検証て ops が異なる値になることを表している．まず，

図 7 に注釈付きの deposit プログラムを示す．de-parameter が Left の場合，ops が空のオペレーショ

posit プログラムは金銭の預け入れと引き出しを行う

ンのリストであることを保証している．一方，Right

プログラムである．以下，プログラムの説明を行う．

の場合，コントラクトの変換結果でさらに分岐する．

1 行目から 3 行目にかけて parameter の型宣言を行

コントラクトの変換が成功した場合，現在の内部取なっている．Left は金銭の預け入れを，Right は引引を開始したアカウントのアドレスとストレージにき出しを表している．5 行目から 11 行目が main 関数

保存されているアドレスが一致するならば，ops は変日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集
1

type parameter =2| Left of tz

3| Right of tz

9

4
5
6

let [@entry] main env parameter storage =let ops =7

match parameter with8

| Left _ -> []9| Right amount ->10

let sender = Glo b al .g e t_ sen der env in

11

if Address.eq sender storage then12

let source_contract = Option.get (C o nt r ac t .c o n t r a c t sender ParamUnit ) in13

[ O p e r a t i o n . t r a n s f e r _ t o k e n s ParamUnit amount s ou rce_contract ]

14
15
16
17
18
19

else failwith ( )inops, storage( * @ ops, stg = main env param storage
ensures
let sco = Con t ra ct. con tra ct (G lo b al . ge t _ s e n d e r env ) ParamUnit in20

match param, sco with21

| Left _, _ ->22

| Right amount, Some sc ->23

ops = []

Address.eq (G lo b al . ge t _s e nd e r env ) storage -> ops = ( O p e r a t i o n . t r a n s f e r _ t o k e n s ParamUnit amountsc ) :: []

24
25
26

| Right _, None -> false
raisesInvalid_a r gu me nt _ ->27

match (C on t ra c t. c on t ra c t (G l ob a l. g et _ s e n d e r env ) ParamUnit ) with28

| None -> true

29
30
31

| Some _ -> false
raisesFail ->

32

match param with33

| Left _ -> false

34| Right _ -> not (Address.eq (G l ob a l. g e t _ s e n de r env ) storage ) *)図7

deposit.ml（注釈付き）

換の結果得られたコントラクトに Right で指定した

4. 3 vote プログラムの検証

金額だけ送金するオペレーションと一致することを

図 8 に注釈付きの vote プログラムを示す．vote プ保証する．変換が失敗して結果が None である場合，ログラムは投票システムを実装したものである．以下，true で例外の発生を表している．25 行目の raises

プログラムの説明を行う．1 行目から 5 行目にかけ

節では例外事後条件を記述する．Invarid argumentて config の型宣言を行う．config は投票タイトルが発生した場合，現在の内部取引を開始したアカウ

title と投票の開始時刻 beginning time，終了時刻

ントのアドレス Global.get sender env の Unit 型

finish time から構成される．続く 7 行目から 11 行のコントラクトへの変換が失敗して，結果が None で目にかけて storage の型宣言を行う．storage は先あったを保証する．また，30 行目でも同様に例外事ほど定義した config と候補者のリスト candidates，

後条件を記述しており，Fail が発生した場合，現在投票済みのアカウントのアドレスのリスト voters かの内部取引を開始したアカウントのアドレスとストら構成される．そして，13 行目以降が vote 関数のレージに保存されているアドレスが一致しないこと定義である．引数の name は投票する候補者の名前を保証する．

を指定する．14 行目の Global.get now env は，コントラクト実行時の時間を取得するための命令であ日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

10
1

type config =2{ title3; beginning_time : timestamp

4; finish_time

5}: string: timestamp

6
7

type storage =8{ config

9; candidates : (string, int ) map

10; voters

11}: config: address set

12
13
14

let vote (env : Env.t ) (name : string ) (storage : storage ) =let now = Global.get_now env in

15

myassert (Timestamp.le s t o r a g e . c o n f i g . b e g i n n i n g _ t i m e now && Timestamp.lt now s t o r a g e . c o n f i g . f i n i s h _ t i m e ) ;16

let addr = G l ob al . get _ so urc e env in

17

myassert (not (Set.mem addr storage.voters ) ) ;18

let x = match Map.get String.eq name s to r ag e . c a nd i da t e s with

19

| Some i -> i20
21

| None -> 0
in

22([] : operation list ) ,23{ config = st orage. config

24; candidates = Map.update String.eq String.lt name (Some (x + 1) ) s to r ag e .c a nd i da t es

25

; voters = Set.update Address.eq Address.lt addr true storag e.voters

26
27
28

}
( * @ ops, stg = vote env name storage
ensures29

let now = Global.get_now env in

30

Timestamp.le s t o r a g e . c o n f i g . b e g i n n i n g _ t i m e now &&31Timestamp.lt now s t o r a g e . c o n f i g . f i n i s h _ t i m e &&32

not Set.mem (G lo b al . ge t _s o ur c e env ) storage.voters ->33

ops = [] &&

34

stg =

35

let addr = G lo bal .g e t_s our ce env in36

let x = match Map.get String.eq name st o r a g e . c an d id a t e s with Some i -> i | None -> 0 in

37

{ storage with38

candidates = Map.update String.eq String.lt name (Some (x + 1) ) st or a ge . ca n di d at e s

39; voters

40

}

41

raises= Set.update Address.eq Address.lt addr true storage.voters

42

Fail ->

43

let now = Global.get_now env in44

not ( Timestamp.le s t o r a g e . c o n f i g . b e g i n n i n g _ t i m e now &&45

Timestamp.lt now s t o r a g e . c o n f i g . f i n i s h _ t i m e &&46

not Set.mem (G lo b al . ge t _s o ur c e env ) storag e.vote rs ) *)図8

vote.ml（注釈付き）

る．15 行目では，取得した時間が投票期間内である

る場合例外を返す．18 行目では候補者のリストからことを調べ，そうでなければ例外を返す．16 行目のname を検索し，得票数を取得する．見つからない場

Global.get source env は，現在のコントラクトを

合は得票数は 0 とする．22 行目は返すオペレーショ

開始したアカウントのアドレスを取得するための命令ンのリストを示しており，空のオペレーションのリである．17 行目ではそのアドレスが投票済みのアカストが指定されている．23 行目以降は更新後のスト

ウントのリストに含まれているかを調べ，含まれていレージを示しており，候補者のリストは name の得票日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集
1
2( * @ ops, stg = vote env name storage
ensures3

let now = Global.get_now env in

4Timestamp.le s t o r a g e . c o n f i g . b e g i n n i n g _ t i m e now &&5Timestamp.lt now s t o r a g e . c o n f i g . f i n i s h _ t i m e &&6

not Set.mem (G lo b al . ge t _s o ur c e env ) storage.voters ->7

forall nm. (match (Map.get String.eq nm stg.ca ndidat es ) with

8

| Some cv -> true

9

| None -> false )10-> (match (Map.get String.eq nm st or a ge . ca n d i d a t e s ) , (Map.get String.eq nm stg.candidates ) with

11

| Some pv, Some cv ->

12
13
14
15

11

if String.eq name nm then pv + 1 = cv else pv = cv
| None, Some cv -> String.eq name nm && cv = 1| _, _ -> false )raises16

Fail ->

17

let now = Global.get_now env in18

not ( Timestamp.le s t o r a g e . c o n f i g . b e g i n n i n g _ t i m e now &&19Timestamp.lt now s t o r a g e . c o n f i g . f i n i s h _ t i m e &&20

not Set.mem (G lo b al . ge t _s o ur c e env ) storag e.vote rs ) *)図9

vote.ml（注釈その 2）

数を 1 増やし（元々リストにない場合は，候補者を追様を記述することも可能である．前と異なる箇所は加して得票数を 1 とする），投票済みのアカウントのensures 節の部分で，具体的には 7 行目から 14 行目

アドレスのリストに現在のコントラクトを開始したアが変更されている．ここでは，投票前と投票後の得票

カウントのアドレスを追加する．27 行目以降は仕様数の差が高々1 であることを保証している．具体的にを GOSPEL で記述したものである．まず，27 行目で見ると，7 行目から 9 行目にかけて任意の文字列 nm

は vote 関数の引数を env，name，storage，返り値に対して，更新後のストレージ stg の候補者のリスを ops，stg と対応付けている．28 行目の ensuresトに含まれている氏名と一致することを仮定してい節で事後条件を記述している．まず，コントラクト実る．この場合に保証される条件が 10 行目から 14 行

行時の時間が投票期間内であること，かつ現在のコン目に記述されており，nm の得票数を投票前後で比較

トラクトを開始したアカウントのアドレスが投票済

すると，name と一致する場合は 1 増えており，そうみのアカウントのリストに含まれていないことを仮でない場合変化がないことを保証している．また，投定する．この時，ops が空のオペレーションリストで票前のストレージ storage には nm に一致する候補者あり，かつ更新後のストレージ stg が，候補者のリがいない場合があり，その場合は投票後の得票数は 1

ストの name の得票数が 1 増えて，投票済みのアカウ

であることを保証する．

ントのアドレスのリストに現在のコントラクトを開始したアカウントのアドレスが追加されている状態

5 関連研究であることを保証する．41 行目の raises 節では例

Tezos のスマートコントラクトの安全性を保証する

外事後条件を記述する．Fail が発生した場合，コンための形式検証手法に，Nishida らの Helmholtz [8]トラクト実行時の時間が投票期間外であること，またが挙げられる．Helmholtz は Tezos のスマートコ

は現在のコントラクトを開始したアカウントのアド

ントラクトを記述するための言語 Michelson [10] にレスが投票済みのアカウントのリストに含まれてい対して，形式検証の手法で自動検証を行う検証器であることを保証する．

る．仕様を表現する注釈を加えた Michelson のプロ

また，同様のプログラムに対して図 9 のように仕グラムから検証条件を生成して，SMT ソルバーがそ日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

12
1

parameter unit ;2storage unit ;3<< ContractAnnot { ( param , st ) | True } - >4{ ( ops , st ’) | amount = 0 && ops = [] ||5amount <> 0 && ( match contract_opt source with6

| Some c - > ops = [ Transfer Unit amount c ]78| None - > False ) }& { _ | False } >>

9

code

/* ( param , st ) */10

{ CDR ;/* st */11

NIL operation ;/* [] ▷ st */12

AMOUNT ;/* amount ▷ [] ▷ st */13

PUSH mutez 0 ;/* 0 ▷ amount ▷ [] ▷ st */14

IFCMPEQ

15{}/* [] ▷ st

( amount ≤ 0) */16{/* [] ▷ st

( amount > 0) */17

SOURCE ;/* src ▷ [] ▷ st */18

CONTRACT unit ;/* Some ( Contract src ) ▷ [] ▷ st */19

ASSERT_SOME ;/* ( Contract src ) ▷ [] ▷ st */20

AMOUNT ; UNIT ;21/* Unit ▷ amount ▷ ( Contract src ) ▷ [] ▷ st */22

TRANS FER_TOKENS ;23/* ( Transfer Unit amount ( Contract src ) ) ▷ [] ▷ st */

24

CONS

25

/* [ Transfer Unit amount ( Contract src ) ] ▷ st */

26

} ;

27

/* ops ▷ st */28

PAIR }/* ( ops , st ) */図 10

boomerang.tzの成否を判断して，プログラムが仕様を満たすか否か

Tezos におけるスマートコントラクトの挙動を定理を判断する．実際に口座への送金や電子署名のチェッ

証明支援系 Coq でモデル化し，その性質を検証する

クなど多くのスマートコントラクトの検証に成功し手法が提案されている [2] [4]．これらの手法においてている．

は全自動で検証を行うことを目標とする本論文の手本論文では Michelson より高水準な言語である

法と異なり，検証は Coq を用いて手動で行われる．

SCaml に対する検証手法を提案した．SCameleer は
高水準言語に対して直接的に仕様記述ができ，検証

6 まとめと今後の課題が可能であるという点での有用性がある．一方で本

本論文では OCaml 互換なスマートコントラクト記

論文の枠組みでは SCaml コンパイラの正しさ自体は

述言語 SCaml のための自動検証器 SCameleer を提仮定しているため，生成された Michelson プログラ

案した．SCameleer は OCaml のための演繹的検証器

ムの正しさは SCaml コンパイラの正しさに依存してCameleer の拡張として実装されており，GOSPELいる．本論文による手法と，生成された Michelson

言語を用いて与えた仕様をプログラムが満たすことをコードに対する Helmholtz を用いた検証とを組み検証する．拡張にあたって，Cameleer を SCaml の合わせることで，より高度な安全性が実現されると期標準ライブラリを扱えるように拡張した．また，実装待される．SCameleer における GOSPEL で記述さした SCameleer が正しく SCaml のプログラムを検れた仕様から，自動的に Helmholtz で扱うことの証することができることを，いくつかのスマートコンできる仕様記述を取り出すことにより，このワークフ

トラクトを例に挙げ確かめた．

ローをより簡便化することは，今後の課題である．

今後の課題は大きく分けて二つあると考える．一つ

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集
目は安全な Michelson のプログラムへの変換手法の確立である．SCaml は Michelson にコンパイルされブ
ロックチェーン上で実行されるという性質上，SCamlのプログラムが持つ性質を変換先の Michelson のプ
ログラムが引き継ぐことを保証し，その安全性を担保する必要がある．そのために，Michelson のための形式検証器 Helmholtz [8] で扱える仕様を SCaml に付加した GOSPEL による記述から自動的に得る方法を検討している．もう一つが SCameleer の利便性の向上である．現在の SCameleer は SCaml の標準ライブラリの一部の機能が未実装であり，検証できる

SCaml のプログラムの数が限られている．したがってこれらを実装して，さらに多くのスマートコントラ
クトを検証することで，SCameleer の実用性を高めることが必要である．
謝辞本研究はテゾス財団からの助成金を受けて行われた．

参 考 文 献[ 1 ] Allombert, V., Bourgoin, M., and Tesson, J.: Introduction to the Tezos Blockchain, 17th International Conference on High Performance Computing& Simulation, HPCS 2019, Dublin, Ireland, July
15-19, 2019, IEEE, 2019, pp. 1–10.
[ 2 ] Annenkov, D., Nielsen, J. B., and Spitters,
B.: ConCert: a smart contract certiﬁcation framework in Coq, Proceedings of the 9th ACM SIGPLAN International Conference on Certiﬁed Programs and Proofs, CPP 2020, New Orleans, LA,
USA, January 20-21, 2020, Blanchette, J. andHritcu, C.(eds.), ACM, 2020, pp. 215–228.
[ 3 ] Barrett, C. W., Conway, C. L., Deters, M.,
Hadarean, L., Jovanovic, D., King, T., Reynolds,
A., and Tinelli, C.: CVC4, Computer Aided Veriﬁcation - 23rd International Conference, CAV 2011,
Snowbird, UT, USA, July 14-20, 2011. Proceedings,
Gopalakrishnan, G. and Qadeer, S.(eds.), Lecture
Notes in Computer Science, Vol. 6806, Springer,
2011, pp. 171–177.
[ 4 ] Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B.,
and Tesson, J.: Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts, Formal Methods.
FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers,

13

Part I, Sekerinski, E., Moreira, N., Oliveira, J. N.,
Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M.,
Marmsoler, D., Campos, J., Astarte, T., Gonnord,
L., Cerone, A., Couto, L., Dongol, B., Kutrib, M.,
Monteiro, P., and Delmas, D.(eds.), Lecture Notes
in Computer Science, Vol. 12232, Springer, 2019,
pp. 368–379.
[ 5 ] Conchon, S., Coquereau, A., Iguernlala, M., andMebsout, A.: Alt-Ergo 2.2, SMT Workshop: International Workshop on Satisﬁability Modulo Theories, Oxford, United Kingdom, July 2018.
[ 6 ] de Moura, L. M. and Bjørner, N.: Z3: An Efﬁcient SMT Solver, Tools and Algorithms for theConstruction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Partof the Joint European Conferences on Theory andPractice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Ramakrishnan, C. R. and Rehof, J.(eds.), Lecture
Notes in Computer Science, Vol. 4963, Springer,
2008, pp. 337–340.
[ 7 ] Filliâtre, J. and Paskevich, A.: Why3 - Where
Programs Meet Provers, Programming Languages
and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practiceof Software, ETAPS 2013, Rome, Italy, March
16-24, 2013. Proceedings, Felleisen, M. and Gardner, P.(eds.), Lecture Notes in Computer Science,Vol. 7792, Springer, 2013, pp. 125–128.
[ 8 ] Nishida, Y., Saito, H., Chen, R., Kawata, A., Furuse, J., Suenaga, K., and Igarashi, A.: Helmholtz:
A Veriﬁer for Tezos Smart Contracts Based on Reﬁnement Types, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Partof the European Joint Conferences on Theory andPractice of Software, ETAPS 2021, Luxembourg
City, Luxembourg, March 27 - April 1, 2021,
Proceedings, Part II, Groote, J. F. and Larsen,
K. G.(eds.), Lecture Notes in Computer Science,Vol. 12652, Springer, 2021, pp. 262–280.
[ 9 ] Pereira, M. and Ravara, A.: Cameleer: A Deductive Veriﬁcation Tool for OCaml, Computer
Aided Veriﬁcation - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021,
Proceedings, Part II, Silva, A. and Leino, K.
R. M.(eds.), Lecture Notes in Computer Science,Vol. 12760, Springer, 2021, pp. 677–689.
[10] TezosDeveloper: Michelson: the language ofSmart Contracts in Tezos, https://tezos.gitlab.
io/alpha/michelson.html. (Accessed on July 6th,2022).