Cardanoにおけるスマートコントラクト検証の新時代

Cardanoでは、スマートコントラクトはPlinth、Aiken、Plu–tsなどの強力な表層言語で作成される。これらのコントラクトは現実の貴重な資産をコントロールする。失敗した場合、資金は盗まれたり永久にロックされたりする可能性がある。

Input | Output (IO)は、Cardanoスマートコントラクトに形式検証をもたらす新しいツールを開発している。AGDA、ROQ（旧Coq）、その他の証明支援系のようなシステムに基づくエコシステム内の既存のツールは強力な保証を提供しているが、一般的に使用するには専門知識が必要である。この新しいツールはLean4証明系とZ3のようなSMTソルバーを組み合わせて、コントラクトが意図したとおりに動作するかを自動的にチェックする。その目標は、開発者が自分で形式証明を記述する必要性をなくすことである。

このツールが画期的なのは、完全自動化という点である。手動による証明も、専門家の介入もない。ボタンをクリックするだけで、形式検証を実行できる。つまり、CI/CDパイプラインに直接統合し、コミットごとにコントラクトの形式検証ができる。即座に、継続的に、手頃な価格で。このツールは現在も開発が続いており、準備が整い次第利用可能になる予定だ。

形式検証を行う理由

テストがカバーするのは、思いつける範囲のケースまたはシナリオのみだ。プロパティベーステストは非常に役立つが、テスト領域の大部分はチェックされないままとなる。さらに、複数のシナリオと攻撃の探索を含む包括的なテストスイートは、一般に多大な開発努力を必要とし、テスト目標が極めて多数かつ複雑な場合は支えきれなくなることもある。

形式検証では、コントラクトのプロパティを提示すれば、それらが実際に常に真であることを証明できる。形式検証技法の中には、ある性質が検証されないときに反例を生成することができるものもある。エコシステム内の既存の形式検証ツールは、セキュリティと正確性の保証には問題ないが、異なる言語でのモデル開発に依存し、非常にニッチな専門知識を必要とする場合が少なくない。複雑で自動化が進んでおらず、再利用可能な反例も生成できないため、ほとんどの開発者には使いこなせない。

私たちが目指していること

IOの自動形式検証ツールは、以下の方法でスマートコントラクトを検証仕様としている。

1. プログラミング言語（Plinth、Aiken、Plu-ts、UPLCなど）からLean4の内部表現に自動変換し、忠実な意味モデルを作成する。
2. ントラクトプロパティをLean定理として変換する。コントラクトプロパティはUniversal Annotation Languageで記述され、複数言語間での仕様を可能にする。
3. Leanの表現と定理を、扱いやすい、しかし同等のSMTクエリに変換し、簡略化する。
4. この表現を強力なSMTソルバー（Z3、CVC5など）に渡す。
5. 結果は、プロパティが成立することを示す再現可能な証明、問題を引き起こす具体的な実行経路を示す再現可能な反例、ソルバーが判断できない場合に専門家が手動で解決すべき証明義務のいずれかとなる。

このツールは、最適化、簡略化、Cardano固有の知識をコアに広範に組み込むことで、専門家による介入の必要性を最小限に抑えるように設計されている。

開発状況

現在、推論の中核部分のバージョンは強力になっている。非常に専門的な最適化、簡略化、正規化のための書き換えルールが多数実装されており、これによって現実的なCardanoのスマートコントラクト関数にも対応できることを示している。私たちが開発したツールを使っても、開発者が好みのプログラミング言語で利用できる表層言語の多くの高レベルな機能を制限しないよう、考慮している。

また、Lean4の目標をSMTクエリに変換する、SMTバックエンドへの翻訳機能と、反例をLeanに戻すためのメカニズムを構築した。

シンプルな例

現在、私たちは、どのプログラミング言語からであってもLean4へのトランスペラーは持っていないが、Lean4の例でツールを実演することは可能だ。そこで、VacuumLabsのCapture the Flagのべスティング例を、手動でLean4に翻訳した。

以下のバリデーターは、べスティングコントラクトにロックされた資金が、受益者がトランザクションに署名し、べスティング期間が経過した場合にのみ使用できることを検証する。

def validator : Demo -> VestingDatum -> VestingRedeemer -> ScriptContext -> Bool :=
    fun demo datum _ sc =>
        let transaction := sc.transaction;
        let purpose := sc.purpose;
        let signatories := transaction.signatories;
        let v_range := transaction.validity_range
        (purpose == Purpose.Spending) && (containsKey signatories datum.beneficiary demo) && (timeHasElapsed v_range datum.lock_until)

2つのヘルパー関数が使用されている。ヘルパー関数containsKeyは受益者の鍵が与えられたリストにあることをのみ検証する。その定義は以下の通りだ。

def containsKey : List VerificationKeyHash -> VerificationKeyHash -> Bool :=
   fun keys key =>
   match keys with
   | [] => false
   | k :: ks => if k == key then true else containsKey ks key

ヘルパー関数timeHasElapsedは、ベスティング期間が経過したことを確認する。その定義は以下となる。

def timeHasElapsed : ValidityRange -> POSIXTime -> Bool :=
    fun range time =>
        range.upper_bound >= time.time

これは、開発者がCardanoのスマートコントラクトプログラミング言語のいずれかを使用して記述するであろうコードと非常に似通っている。

コードが期待される要件に準拠していることを検証するために、テスター（あるいは開発者自身）は、通常、正常系シナリオおよびエッジケースシナリオを複数作成する必要がある。

しかし、私たちの手法を使えば、彼らは意図された振る舞い（すなわち、満たされるべきプロパティ）を指定するだけで済む。

その期待される振る舞いは、Lean4の定理として表現することができる。現段階ではこの言語はまだそれほど使いやすいものではないが、今後改善していく予定だ。

theorem only_accept_if_signatory_and_time_elapsed :
    ∀ (datum: VestingDatum) (redeemer: VestingRedeemer) (scriptContext : ScriptContext) (time: POSIXTime),


    (isValidCtx scriptContext time) →  
    (validator  datum redeemer scriptContext) →


    (scriptContext.transaction.signatories.contains datum.beneficiary
    &&
    time.time ≥ datum.lock_until.time)

この定理は単純に、データ、リディーマー、スクリプトコンテキストに関わらず、現在の時刻timeが有効範囲内にあり、かつバリデーターがtrueを返した場合、以下の条件が満たされていなければならない、と述べている。 

1. トランザクション署名者に、データにある受益者が含まれていること
2. 現在の時刻がデータで指定された時刻よりも後であること

私たちのツールは自動的にこれをSMTクエリ（開発者が読むことを想定していない）に変換し、SMTソルバーに送信する。

するとSMTソルバーは定理が「偽である」と報告する。そしてツールは、以下のテストケース（読みやすくするために少し整理してある）を生成する。

❌ Falsified
Counterexample:
 - datum:
{ lock_until: 1,
	  Beneficiary: 0}
 - time:
0
 - scriptContext:
{ …
  purpose: Spending,
	  …
  signatories: [0],
  …
  validity_range : [0, 11798],
  …}
 - redeemer: 8335

この反例はtimeHasElapsed述語のテストが間違っていることを示している。実際、有効範囲の上限が十分に高ければ（例えば11798。この数値はソルバーがちょっとやりすぎた感は否めないが）は、たとえ時間が実際に経過していなくても（ここでは時間は0、ロックは1まで）、受益者が資金のロックを解除するのに十分となってしまう。

このシナリオ、つまり有効範囲の上限を非常に高く設定したケースは、このCapture the Flagを解くために、VacuumLabsの例で再現することもできる。

今後の展望

本稿はブログシリーズ第1弾となる。次の記事では、さらに深く掘り下げて、CEKマシンとPlutus CoreをLean4で再実装することで、UPLCコードを自動的に証明する方法を紹介する。このメカニズムを本番環境のコードで実演し、このツールがコードレベルで行われた最適化を形式的に証明するためにも使用できる方法を示す。