レベルアップしたCardanoのスマートコントラクト検証で、かつてない恒常的な安全性を実現

Cardanoノードで実行されるスマートコントラクトを実際のレベルで形式検証することが可能になり、抽象モデルや表層ループで推論するのではなく、UPLC（Untyped Plutus Core）を直接操作することができるようになった。 

UPLCを直接対象とすることで、ソース言語を問わずコントラクトの検証が可能になる。これには、Plinth、Aiken、Plutarchの他、Plutus Coreコンパイルパイプラインを対象とする将来の言語も含まれる。

UPLCレベルにおけるここまでの証明自動化と分析は、これまでCardanoで実現されたことはない。 

このアプローチは、スマートコントラクト保証における大きなギャップを埋める。コンパイラーがセマンティックスを保持していると仮定したり（いくつかの最適化に成功した後でさえ）、ソースコードやモデルレベルでの検証がすべての問題を捕捉していると仮定する代わりに、誰でも実際にコンパイルされた（あるいはデプロイされた）バイトコードを直接検証することができる。 

このシリーズの最初のブログ記事で示したように、プロパティには表層言語レベルでアノテーションが付けられることが期待されている。そして、トランスパイラーは対応するUPLCコードとLean4形式化を生成する。 

Input | Output Engineering (IOE)の形式検証ツールは、スマートコントラクトの正しさを自動的に証明し、セキュリティの脆弱性がないことを保証するだけでなく、具体的な反例を生成する機能も提供する。プロパティが満たされなかった場合、ツールは問題を引き起こしたデータム、リディーマー、およびスクリプトコンテキストを特定する。逆に、プロパティが保持されていることが証明されたとき、ソース言語に関係なく、デプロイされたコントラクトの動作について数学的な確実性が提供される。

検証のギャップ

すべてのCardanoスマートコントラクトは実行前にUPLCにコンパイルされる。しかし、形式検証は従来、より高い抽象化レベルで運用されてきた。つまり、コントラクトそのものよりも、コントラクトモデルを確認するものだった。

これにより、死角が生じることになる。すなわち、コンパイラーの変換、最適化パス、わずかなセマンティクスのシフトによって、モデル抽象化やソースコードレベルの検証では見逃してしまう問題を引き起こす可能性がある。本シリーズの前回の記事では、Lean4での動作を検証することで、スマートコントラクトのバグをツールが自動的に検知する仕組みについて解説した。今回は、実際にオンチェーンで動作するコードを直接操作するために、機能がどのように拡張されたかについて説明する。

Lean4でのUPLC実行の構築

Cardanoのコントラクトを形式検証するためには、Lean4でUPLCとその実行セマンティクスを一から忠実に再実装する必要があった。これは、Plutus Coreの型と用語の包括的なエンコーディング、CEK（Control Evaluation Kontinuation）マシンの完全な実装（現在はコストモデルを簡素化している）、さまざまな組み込みのすべてを含めながら、Haskell実装に可能な限り近づけたものだ。

CEKマシンは、オンチェーン検証中にUPLCコードを評価する仮想マシンである。Lean4で再実装することで、実際の検証中にスマートコントラクトがどのように実行されるのかについて、ステップごとの形式的な推論が可能になる。

任意のUPLCソースからの自動トランスパイレーション

このツールには、その出所に関係なく、生のUPLCを自動的にLean4 UPLC表現にトランスパイルするコマンドが含まれている。したがって、ユーザーが個別のモデルを作成したり、スマートコントラクトを手動でLean4に変換したりする必要がない。 

プロパティが満たされない場合の具体例

この形式検証ツールの中心的な強みの1つは、プロパティを証明するだけでなく、プロパティが満たされない場合の具体例（反例）が発見できる点にある。

UPLCコードに対してプロパティを検証する際、そのツールは単にCEKマシンを通じて対話的に帰納ステップを実行するだけではない。一連の最適化ルールを適用することによってCEK STEP関数を系統的に簡略化し、指定されたスクリプト予算に関するコントラクトの動作について、コンパクトで意味論的に等価な表現を生成する。

def step (Sigma : State) : State :=
  match Sigma with
  | s; ρ ▷ u(var x) => s ◁ ρ⟦x⟧ If x is bound in ρ
  | s; ρ ▷ u(con T c) => s ◁ v⟨con T c⟩
  | s; ρ ▷ u(lam x, M) => s ◁ v⟨lam x, M, ρ⟩
  | s; ρ ▷ u(delay M) => s ◁ v⟨delay M, ρ⟩
  | s; ρ ▷ u(force M) =>  (@f(force ⎵) ⋅ s); ρ ▷ M
  | s; ρ ▷ u[M ∘_ N] => (@f[⎵ (N, ρ)] ⋅ s); ρ ▷ M
  | s; ρ ▷ u(constr i (M ⋅ Ms)) => (@f(constr i, [] ⎵ (Ms, ρ)) ⋅ s); ρ ▷ M
  | s; ρ ▷ u(constr i []) => s ◁ v⟨constr i, []⟩
  | s; ρ ▷ u(case N, Ms) => (@f(case ⎵ (Ms, ρ)) ⋅ s); ρ ▷ N
  | s; ρ ▷ u(builtin b) => s ◁ v⟨builtin b, [], α(b)⟩
  | s; ρ ▷ u(error) => ◆
  | [] ◁ V => ▢ V
  | (@f[⎵ (M, ρ)] ⋅ s) ◁ V => (@f[V ⎵] ⋅ s); ρ ▷ M
  | (@f[v⟨lam x, M, ρ⟩ ⎵] ⋅ s) ◁ V => s; ρ⟦x ↦ V⟧ ▷ M
  | (@f[⎵ V] ⋅ s) ◁ v⟨lam x, M, ρ⟩ => s; ρ⟦x ↦ V⟧ ▷ M
  | (@f[v⟨builtin b, Vs, ι ⊙ η⟩ ⎵] ⋅ s) ◁ V =>
(s ◁ v⟨builtin b, Vs :⋅ V, η⟩) If ι ∈ 𝓤 ∪ 𝓥
  | (@f[⎵ V] ⋅ s) ◁ v⟨builtin b, Vs, ι ⊙ η⟩ =>
(s ◁ v⟨builtin b, Vs :⋅ V, η⟩) If ι ∈ 𝓤 ∪ 𝓥
  | (@f[v⟨builtin b, Vs, a[ι]⟩ ⎵] ⋅ s) ◁ V =>
(Eval_CEK(s, b, Vs :⋅ V)) If ι ∈ 𝓤 ∪ 𝓥
  | (@f[⎵ V] ⋅ s) ◁ v⟨builtin b, Vs, a[ι]⟩ =>
(Eval_CEK(s, b, Vs :⋅ V)) If ι ∈ 𝓤 ∪ 𝓥
  | (@f(force ⎵) ⋅ s) ◁ v⟨delay M, ρ⟩ => s; ρ ▷ M
  | (@f(force ⎵) ⋅ s) ◁ v⟨builtin b, Vs, ι ⊙ η⟩ =>
(s ◁ v⟨builtin b, Vs, η⟩) If ι ∈ 𝓠
  | (@f(force ⎵) ⋅ s) ◁ v⟨builtin b, Vs, a[ι]⟩ =>
(Eval_CEK(s, b, Vs)) If ι ∈ 𝓠
  | (@f(constr i, Vs ⎵ (M ⋅ Ms, ρ)) ⋅ s) ◁ V =>
(@f(constr i, Vs :⋅ V ⎵ (Ms, ρ)) ⋅ s); ρ ▷ M
  | (@f(constr i, Vs ⎵ ([], ρ)) ⋅ s) ◁ V => s ◁ v⟨constr i, Vs :⋅ V⟩
  | (@f(case ⎵ (Ms, ρ)) ⋅ s) ◁ v⟨constr i, Vs⟩ => unfoldCase s i Ms Vs ρ
  | _ => ◆

最終的に得られるのは、コントラクトの動作を考えうるすべての入力にわたって捉えた、高度に最適化され、簡略化された SMT（充足可能性モジュロ理論）の論理式である。このツールの事前処理フェーズは、提供されたUPLCプログラムに基づき、CEKマシンの評価と簡約のルールを最終的な論理式に完全に解決しようと試みる。本質的には入力と出力に関する直接的な論理制約のみが残るが、これはコード内で参照されているUPLC組み込み関数から導出されたものだ。ただし、スクリプト予算の計算が特定のUPLC組み込みデータ型の値に依存する場合、CEKの枠組みのごく一部が最終的な解に残ることもある。 

あるプロパティが満たされない（違反する）場合、SMTソルバーは、与えられた入力でスマートコントラクトを一度実行した際に、プロパティ違反を引き起こす反例を生成する。他の形式手法技法とは異なり、これは単なる証明の失敗ではない。このツールは、プロパティ違反につながる具体的なデータ、リディーマー、およびスクリプトコンテキストを返す。

以下は、2つの整数を加算するUPLCプログラム例であり、実行を簡略化する方法を示している。 

(program 1.1.0 (lam x (lam y [[(builtin addInteger) y] x] )))

チームは、UPLCファイルを読み取り、それをLeanの定義としてロードするために必要なツールを構築した。また、評価結果を評価し、ユーザーにわかりやすい表現（Bool、Integer、Pairsなど）で返すのに役立つ多くのライブラリー関数を定義した。

#import_uplc "Tests/addInteger.uplc" addInteger

def executeAdd (x : Integer) (y : Integer) : Option Int :=
 executeIntProgram addInteger (intArgs2 x y) 20

この時点から、デフォルトのLeanのeval関数を使って、いくつかの入力でUPLCプログラムを評価することができる。

#eval executeAdd 55 110

このプログラムの正しさを形式的に証明するために、ツール#solveを使用することもできる。

#solve [∀ (x y : Integer), executeAdd x y = some (x + y)]

この正しさを証明するために、このプログラムはCEKステップ関数を20回実行する必要があるため、単純な展開では非常に非効率となる。代わりに、addIntegerが実際に2つの入力に対して加算を実行することを示すために、#solveコマンドが呼び出されたときに以下のSMTクエリが生成される。

; Setting the solver call
(set-option :print-success true)
(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :smt.pull-nested-quantifiers true)
(set-option :smt.mbqi true)

; Type declaration
(declare-fun @isInt ( Int) Bool)

; Variable declaration
(declare-const $0 Int)
(declare-const $1 Int)
(declare-const $2 Int)

; Option declaration
(declare-datatype @Option (par ( |@α|) ( (Option.none )
 (Option.some  (Option.some.1 |@α|)))))

; Program and specification 
(define-fun @isOption._uniq.32834 ((@x (@Option  Int))) Bool (ite (is-Option.some @x) (@isInt (Option.some.1 @x)) true))

(assert (not (=> (@isInt $0) (=> (@isInt $1) (=> (@isInt $2) (=> (not (< $0 0)) (=> (= ((as Option.some (@Option  Int)) $2) ((as Option.some (@Option  Int)) (+ $0 $1))) (= $2 (+ $0 $1)))))))))

見ての通り、CEKステップ関数を20回繰り返すとしても、プログラムと仕様は強力な最適化ルールによってわずか$0+$1にまで簡約された。

表層論理だけでなく、コンパイルされたコードを検証

UPLCコードを直接対象とする形式検証ツールを使用することで、Cardanoブロックチェーンで実行されるそのままのコード表現でプロパティを証明できる。そのため、このアプローチは表層言語レベルでの仮定や、コンパイルがセマンティクスを正しく保存するとの信頼に依存することはない。

代わりに、このツールは実際のコンパイルされたバリデーターがどのように動作するかを、コンパイラーの最適化と共に検証する。これにより、コンパイルされたコントラクトが（表層コードだけでなく）正しく動作し、変換やコンパイラーの最適化によってバグが発生していないことが確実に保証される。

私たちは、Cardanoメインネットで現在実行されているプロジェクトでツールをテストした。addIntegerの例と同様に、生成されたUPLCコードはコマンド#import_uplcによってLean4に直接インポートされる。

#import_uplc "Tests/Smt/Benchmarks/UPLC/Examples/Onchain/processSCOrder.uplc" processSCOrder
#prep_uplc "compiledProcessSCOrder" processSCOrder [ProcessSCInput] orderInputToParams 5000

processSCOrder関数は単純なものではなく、1,500行を超える整形されたUPLCコードである。#PREP_UPLCコマンドは以下の処理を実行する。まずProcessSCInput型の入力を持ち、orderInputToParams関数を使ってその入力をUPLC組み込み表現に変換するラムダ項を作成する。次に、ラムダ項をUPLCコードに適用したあと、指定されたスクリプト予算（例：5,000実行ステップ）によって制約された一連の最適化を適用する。 

最終的に得られるのはcompiledProcessSCOrderというLean4の定義であるが、私たちはのちにこれを使って、開発チームから提供されたprocessSCOrder関数が満たすべき14の要件を形式化した。

def sto7_part1 (x : ProcessSCInput) : Prop :=
  isBuySCOrder x →
  validOrderInput x →
  x.state.crN_RC = 0 →
  successfulOrderImpliesPredicate (fromHaltState $ compiledProcessSCOrder x) (validBuySC x)

#solve [ ∀ (x : ProcessSCInput), sto7_part1 x ]

ツールは以下を出力する。✅これらすべてに対してvalid。事前処理と最適化ステップにより、各SMTモデルは約60行のSMTLib2で構成される。これら14の仕様の証明時間は、通常のノートPCで約10秒である。

また、UPLCコードにいくつかのバグを注入して、ツールが不適合を検出できるか、続いて証拠として反例を生成できるかを検証した。

 x:=
   scMinRatio : 5/2
   scMinOperatorFee : 1
   scMaxOperatorFee : 3
   scOperatorFeeRatio : 4/4
   scBaseFeeBSC : 2/1
   scBaseFeeSSC : 0/3
   nbTokens : 1
   totalPrice : 4
   orderSubmitter : 7
   orderRate : 1/2
   orderTimeStamp : 13
   orderTxOutRef : 9
   adaAtOrderUtxo : 11
   minAdaTransfer : 3
   state : ComputeReserve.mk 19 5 0

このような反例によって、開発者は簡単にデバッグを実行し、修正を適用してからプルーフを再実行して、修正されたバージョンが想定通りに動作するかどうかを検証することができる。

実用的な意味

この機能により、UPLCに準拠している限り、開発者は入力言語に関係なくコントラクトの微妙なバグを検知することができる。検証プロセスは実際のデプロイされたコントラクトを使って完全に自動で実行される。 

将来的には、このツールを使用して、表層コードとコンパイルされたコードが意味論的に等価であることを検証することができ、コンパイラーが意図した動作を保存していることを数学的に証明できる。このツールは2つの異なるUPLCスクリプトの等価性を証明するためにも使用できるが、ユーザーによる定式化の必要は最小限で済む。 

このツールの開発作業はまだ初期段階にあるものの、すでにテストが行われている。今後のブログ記事では、メインネットで実行されるDAppの証明のために、これが内部的にどのように使われるかを示す。

マルチトランザクションシナリオへの拡張

これまで、単一のトランザクションに焦点を当て、個々のコントラクト実行のプロパティを個別に検証してきた。しかし、多くのスマートコントラクトのバグ（そしてほとんどの実際のビジネスロジック）は、データムが複数のブロックまたはエポックにまたがって進化するマルチステップインタラクションから発生する。

チュートリアルの一般的な例、すなわち、オークション、エスクローコントラクト、ビジネスロジックが異なる利害関係者からの複数のトランザクションを必要とするその他のプロトコルなどを考えてみて欲しい。

このシリーズの次の記事では、複数のトランザクションとブロックにわたるスマートコントラクトの動作を検証するためのステートマシンモデルを紹介する。ブロックチェーンステータスと台帳ルールがどのようにモデル化されたかを示し、有限シーケンスから無限実行までの実行トレースを検証するための新しい技術を提示する予定だ。