スマートコントラクトの形式的検証
最終編集者: , Invalid DateTime
スマートコントラクト は分散型でトラストレスかつ堅牢なアプリケーションの作成を可能とし、それによってユーザーに対して新しいユースケースを導入し、さらなる価値を引き出します。 スマートコントラクトが取り扱うものには巨額の価値があるため、デベロッパーにとってセキュリティは極めて重要です。
形式的検証はスマートコントラクトのセキュリティを向上させるために推奨される技術のひとつです。 形式的検証は、形式手法(opens in a new tab)によってプログラムの仕様記述、設計および検証を行うもので、極めて重要性の高いハードウェアやソフトウェアシステムの正しさを保証するのに以前から使われてきました。
スマートコントラクトに形式的検証を実施することで、スマートコントラクトの挙動があらかじめ規定された仕様を満たすことが証明できます。 スマートコントラクトのコードの正しさを査定する他の手法(テスト技法など)と比べて、形式的検証はスマートコントラクトが機能的に正しいことをより強力に保証します。
形式的検証とは何か
形式的検証というのは、形式仕様記述に対してシステムの正しさを評価するための一連の作業のことです。 簡単に言うと、形式的検証によってシステムの挙動が求められている要件を満たしているかどうかを確かめることができます。
システム(この場合はスマートコントラクト)の期待される挙動は形式的な表現によって記述され、形式的プロパティは仕様記述言語で書かれます。 そして、形式的検証の技法により、スマートコントラクトの実装が仕様に準拠していることを検証でき、さらにその実装の正しさの数学的証明を導くことができます。 スマートコントラクトが仕様を満たすことを、「機能的に正しい」、「設計により正しい」または「構成により正しい」といいます。
形式モデルとは何か
計算機科学において、 計算の形式モデル(opens in a new tab)は計算プロセスを数学的に記述するものです。 プログラムは数学的な関数(方程式)によって抽象化され、関数の入力に対して出力をどう計算するかが形式モデルによって記述されます。
形式モデルは、プログラムの挙動の分析を評価できる水準での抽象化を可能とします。 形式モデルがあることで形式仕様が作成でき、それによって、問題となっているモデルの持つべき望ましいプロパティが記述されます。
形式的検証のためのスマートコントラクトのモデル化には、さまざまな技法が用いられます。 たとえば、スマートコントラクトの高水準な挙動を論証するために用いられるモデルがあります。 その ようなモデル化技法では、スマートコントラクトを与えられた入力に基いて計算を実行するブラックボックスとみなします。
高水準なモデルでは、スマートコントラクトと外部エージェント(外部所有アカウント(EOA)、コントラクトアカウントもしくはブロックチェーン環境)との関係に重点が置かれます。 このようなモデルは、スマートコントラクトが特定のユーザーインタラクションにどう応じるべきかを記述するのに有用です。
逆に、スマートコントラクトの低水準な挙動に重点を置く形式モデルもあります。 高水準なモデルはスマートコントラクトの機能について論証するのに役立ちますが、その反面、実装の内部動作の詳細が上手く掴めないこともあります。 低水準なモデルのプログラム解析ではプログラムをホワイトボックスとみなし、スマートコントラクトの実行に関連するプロパティの論証では、プログラムトレースや制御フローグラフ(opens in a new tab)など、スマートコントラクトアプリケーションの低水準な表現を利用します。
低水準なモデルはイーサリアムの実行環境(EVM)における実際の実行を表すため、理想的であると考えられています。 低水準なモデリング技法は、スマートコントラクトの重要な安全性の確立と潜在的な脆弱性の検出に特に有用です。
形式仕様記述とは何か
仕様とは、特定のシステムが満たすべき技術的要件のことです。 プログラミングにおいては、仕様はプログラムの実行についてのおおまかな狙い(すなわち、プログラムが何をすべきか)を表します。
スマートコントラクトの文脈では、形式仕様記述はスマートコントラクトが満たさなければならない要件を形式的に記述したものであり、これをプロパティと呼びます。 プロパティはスマートコントラクトの実行を通しての「不変条件」として記述され、例外なしにあらゆる状況下で真であるべき論理アサーションを表現するものです。
したがって、形式仕様記述はスマートコントラクトのしかるべき挙動を形式言語で記述したものの集まりである、と考えることができます。 仕様が対象とするのはスマートコントラクトのプロパティで、スマートコントラクトがさまざまな状況下でどのように動作すべきかを表します。 スマートコントラクトがそれらのプロパティ(不変条件) を実行 中に破らないことを見極めるのが、 形式的検証の目的です。
形式仕様記述は、スマートコントラクトのセキュアな実装をする上で極めて重要です。 求められた不変条件を満たさなかったり、実行中にプロパティを破るスマートコントラクトには、その機能を害したり悪用を許してしまう脆弱性があるおそれがあります。
スマートコントラクトの形式仕様記述の種類
形式的仕様記述により、プログラム実行の正しさを数学的に論証することが可能となります。 形式モデルと同様、形式仕様記述は高水準のプロパティもしくはスマートコントラクトの実装の低水準の挙動をとらえることができます。
形式仕様記述はプログラム論理を用いて導出され、それによってプログラムのプロパティが形式的に論証できるようになります。 プログラム論理が備えている形式規則により、プログラムのしかるべき挙動が(数学的に)表現されます。 到達可能性論理(opens in a new tab)、時相論理(opens in a new tab)、ホーア論理(opens in a new tab)を含む様々なプログラム論理が形式仕様記述に用いられます。
スマートコントラクトの形式仕様記述は高水準な仕様記述と低水準な仕様記述に大別されます。 いずれの場合でも、分析対象のシステムのプロパティを適切かつ一義的に記述できなければなりません。
高水準な仕様記述
その名のとおり、高水準な仕様記述(「モデル指向仕様記述」とも呼ばれます) はプ ログラムの高水準な挙動を記述するためのものです。 高水準な仕様記述においてスマートコントラクトは有限状態機械(opens in a new tab)(FSM)としてモデル化されます。スマートコントラクトの挙動は処理の実行を伴う状態遷移で表され、モデルの形式的プロパティは時相論理で記述されます。
時相論理(opens in a new tab)は時間という条件の付いた命題(たとえば、「私はいつも空腹だ」や「私はいずれ空腹になる」)を論証するための規則の集まりです。 形式的検証での時相論理は、状態遷移機械でモデル化されたシステムの正しい挙動に関するアサーションを記述するために使われます。 具体的には、スマートコントラクトがある将来の時点でモデルのどの状態にあるのか、そしてどのように状態間で遷移するのかを時相論理で記述できます。
高水準な仕様記述は一般に安全性 (safety)と活性 (liveness)という、スマートコントラクトの時相に関する重要な 2 つのプロパティを捕えることができます。 安全性とはすなわち「何も悪いことが起こらない」ということで、通常は不変条件によって表されます。 安全性は、デッドロック(opens in a new tab)が起こらないことといった一般的なソフトウェア要件を意味することもあれば、スマートコントラクトのドメイン固有なプロパティ(たとえば関数に対するアクセス制御の不変条件、状態変数の許容値、トークン転送の条件など)を意味することもあります。
例として、「送金しようとしているトークンの量に対し、送金元の口座残高に不足があってはならない」という、 ERC-20 トークンのスマートコントラクトでtransfer()
やtransferFrom()
を呼び出す際の安全性の要求仕様を考えます。 この自然言語で書かれたスマートコントラクトの不変条件は数学的な形式仕様記述に翻訳され、その妥当性が厳密に検査されます。
活性は「何らかの良いことがいずれは起こる」ということを意味し、スマートコントラクトに関しては、するべき処理を滞りなく進められることを示します。 活性の一例として「流動性」が挙げられ、これは、要求に応じてスマートコントラクトが残高を他ユーザーに譲渡できることを意味します。 このプロパティが破られると、パリティウォレット事件(opens in a new tab)で起こったように、あるはずの資産が引き出せなくなります。
低水準な仕様記述
高水準な仕様記述では、有限状態モデルから出発してモデルの望ましいプロパティを記述しました。 一方で、低水準な仕様記述(プロパティ指向仕様記述とも呼ばれます)では、プログラム(すなわちスマートコントラクト)を数学的な関数の集まりからなるシステムとしてモデル化し、そのシステムの正しい挙動を記述します。
簡単に言うと、低水準な仕様記述ではプログラムのトレース を解析し、それに基づいてスマートコントラクトのプロパティを記述することを目指します。 トレースとは、スマートコントラクトの状態変化を伴った関数の実行シーケンスを指します。したがって、低水準な仕様記述ではスマートコントラクト内部の実行の様子についての要求仕様まで記述できます。
低水準な仕様記述は、ホーア型のプロパティもしくはプログラムの実行フローによって与えられます。
ホーア型のプロパティ
ホーア論理(opens in a new tab)は、スマートコントラクトなどのプログラムの正当性を論証するための形式規則を提供します。 ホーア型のプロパティは、ホーアトリプルと呼ばれる{P}c{Q}という形の式で与えられます。cはプログラムで、PとQはそれぞれ正式には事前条件、事後条件と呼ばれる、c の状態についての述語です。
事前条件は関数を正しく実行するために求められる条件を表しています。スマートコントラクトを呼び出す際には、この事前条件が満たされている必要があります。 事後条件は、関数が正しく実行された場合に成立する条件を表しています。関数呼び出しの後はこの事後条件が真となることが期待されます。 ホーア論理の不変条件は、関数の実行中は常に維持されます(すなわち、変化しません)。
ホーア型の仕様記述により、部分正当性もしくは完全正当性が保証されます。 事前条件が関数実行前に真で あり、実行が停止した場合には事後条件も真であるとき、スマートコントラクト関数の実装は「部分正当性を満たし」ます。 完全正当性を証明するには、関数の実行前に事前条件が真であること、実行が終了すること、その際に事後条件が真であることの三つが必要です。
プログラムによっては実行が終わるのに時間がかかったり、そもそも終わらなかったりするので、完全正当性の証明は困難となります。 とはいえ、イーサリアムのガスメカニズムが無限ループを防ぐので、実行が終了するかどうかは議論の余地はあれども理論上の問題点です(実行は正常に終了するか、'ガス不足'のエラーで打ち切られます)。
ホーア論理で作成されたスマートコントラクトの仕様記述は、スマートコントラクト内部の関数やループを実行するために述べられた事前条件、事後条件、不変条件を含みます。 事前条件が関数への誤った入力を許容する場合もあり、その際は事後条件でそのような誤った入力があった場合の応答(例外を発生させるなど)が記述されます。 このようにして、ホーア型のプロパティによってスマートコントラクト実装の正当性を保証する際に有効となります。
多くの形式的検証のフレームワークで、関数の意味的正当性を証明するためにホーア型の仕様記述が使われています。 Solidity のrequire
とassert
ステートメントを使えば、スマートコントラクトのコードにホーア型のプロパティを(アサーションとして) 直接書くこともできます。
require
ステートメントは事前 条件もしくは不変条件を書くのに用いられ、ユーザーから与えられた入力の有効性を確認するのに使われることが多く、その一方でassert
ステートメントは安全性のために必要な事後条件を書くのに使われます。 たとえば、 関数への適切なアクセス制御(安全性プロパティの一例) は、require
ステートメントを使用して、該当する関数を呼び出そうとしているアカウントの識別情報を前提条件チェックすることで実現できます。 同様に、assert
ステートメントで実行後のスマートコントラクトの状態を確認することで、コントラクト内部の状態変数(たとえば、流通しているトークンの総数など)が許容される値であることを示す不変条件を違反しないが保護することがであることを示す不変条件の違反を防ぐことができます。
トレースレベルのプロパティ
トレースベースの仕様記述では、スマートコントラクトの状態を遷移する操作や、操作間にある関係を定義します。 前述したように、トレースは特定の方法でスマートコントラクトの状態を変化させる操作シーケンスです。
このアプローチは、スマートコントラクトのモデルがいくつかの定義済みの状態(状態変数で表されます) および遷移(スマートコントラクトの関数で表されます) を備えた状態遷移系で与えられていることを前提としています。 さらに、 スマートコントラクトの操作的意味論を記述するには、プログラムの実行の流れを図示する制御フローグラフ(opens in a new tab) (CFG) がよく用いられます。 ここで、各トレースは制御フローグラフ上のパスで表されます。
主に、トレースレベルの仕様記述は、スマートコントラクトの内部の実行のパターンを論じる際に用いられます。 トレースレベルでの仕様記述を作成することで、スマートコントラクトに許容される実行パス(すなわち、状態遷移)をアサートできます。 シンボリック実行などの手法を用いれば、形式的モデルで定義されていないパスには実行が進まないことを形式的に検証することができます。
例として、公開されている関数でトレースレベルのプロパティの記述ができるDAOコントラクトを見てみましょう。 ここでは、DAO コントラクトによってユーザーが以下の操作を実行できることとします。