Tezosの正式な検証がDeFiのセキュリティを強化

Tezosは有名なPoSパブリックチェーンとして、その魅力はStaking機能だけにとどまりません。Tezosの形式的認証特性もその主要な技術的利点の一つです。この特性はDeFiアプリケーションのセキュリティを大幅に向上させ、ユーザーのスマートコントラクト資金の安全性に対する信頼を強化します。

DeFiのセキュリティと正式な検証方法

分散型金融の迅猛な発展は多くの開発者の注目を集め、一部の著名な分散型金融プロトコルは累計で数億ドルの資金を引き寄せています。しかし、分散型金融分野は依然として重大な課題、すなわち安全性の問題に直面しています。

この問題の代償は大きく、一部のブロックチェーンプロジェクトのネットワーク効果に悪影響を及ぼしました。ここ数ヶ月の間に、いくつかのDeFiプロジェクトが攻撃を受け、損失は数十万ドルから数千万ドルに及びました。あるプロジェクトは、迅速な自己点検によってバグを発見し、凍結措置を講じることで、より大きな損失を回避しました。

安全性を重視する分散型金融（DeFi）開発者にとって、Tezosの形式的認証ソリューションは、安全性を強化しつつDeFiアプリケーションに力を与えることができます。

従来のインターネットアプリケーションでは、サーバーがハッカー攻撃を受けた場合、ユーザーデータをロールバックするだけで損失を回復できます。そのため、ユーザー体験を重視する従来のアプリケーションは、迅速なイテレーションのために一部の安全性を犠牲にすることができます。しかし、DeFiアプリケーションでは、ブロックチェーンの不変性により、スマートコントラクトが一度展開されて安全上の脆弱性が発生すると、ユーザーに与える損失は巨大で回復不能なものになります。

したがって、分散型金融アプリケーションの開発プロセスには、安全性を確保するために大量のテストと高額な監査が必要であり、これは反対にイテレーションの速度と製品の使いやすさに影響を与えます。さらに、安全監査のコストが高いため、多くの開発者が分散型金融アプリケーションプロジェクトを開始することが難しいです。

ブロックチェーン開発人材の不足は、人手による監査コストが高止まりする原因となっています。そのため、機械支援の検証がますます採用される傾向にあり、その中でも形式的認証手法は安全性を確保するための重要な手段です。

形式的認証とは、数学の形式的手法を用いてアルゴリズムの特性を証明または反証することを指し、主に2つの方法があります：

1. モデル検証：システムのすべての可能な状態を列挙し、一つ一つ検証する。小型システムの完全自動化検証に適用される。

2. 演繹検証：まずシステムコードを抽象的な数学モデルとしてマークし、その後定理を証明します。これは大規模システムに適用可能ですが、システムの運用方法を検証システムが理解できる言語に手動で変換する必要があります。

長い間、コストが高いため、形式化验证の方法は主に学術、国防軍工、航空宇宙などの分野に適用されており、商業分野での適用は少ない。従来のインターネットアプリケーションとブロックチェーンアプリケーションの運用環境には本質的な違いがあるため、その開発プロセスも相応に調整されるべきであり、特に安全性の検証段階への投入比率については重要である。

!

公開ブロックチェーン分野における関数型言語の応用

安全性を確保するために、多くのブロックチェーンプロジェクトは基盤アーキテクチャ、仮想マシン、またはスマートコントラクト言語に関して関数型言語を選択しています。たとえば、Ocaml、Haskell、Erlangなどです。関数型言語は、その厳密な変数型の定義、コンパイル検証、および優れた形式的認証ツールチェーン（例えばCoQ）により、安全分野で高い評価を得ています。一般的な手続き型言語で書かれたコードは、形式的認証を行うために関数型言語で再マークする必要があります。

多くのブロックチェーンプロジェクトの中で、Tezosがサポートするスマートコントラクトの高級言語の種類は最も豊富で、Pascal、Ocaml、Haskellなどのさまざまな関数型言語だけでなく、広く使用されているPython言語も含まれています。それに対して、他のいくつかのプロジェクトは開発者に全く新しい関数型言語を学ぶことを要求しており、これは明らかに開発のハードルを上げています。

マイケルソン語のセキュリティ機能

Tezosはスマートコントラクト言語の設計において革新的なアプローチを採用しました。スマートコントラクトの基盤にはOcamlベースのMichelson言語を使用しており、開発者が実際に接するのはPythonなどの高級言語で、Michelson言語自体を深く理解する必要はありません。この方法は、Michelson言語の安全性と監査可能性、さらにはPythonなどの高級言語の使いやすさを組み合わせています。

Michelsonは、アーキテクチャにおいてEthereumのEVMに似た点があり、どちらもスタック言語であり、オンチェーンストレージを使用し、ガス料金モデルを採用し、チューリング完全である。しかし、MichelsonとEVMの主な違いは：

1. 静的型：すべてのMichelsonスマートコントラクトに入るデータは明確に型を定義する必要があり、型の不一致に関連するプログラムのバグを回避します。

2. 原子計算：Michelsonスマートコントラクトは実行を完了してから他のコントラクトを呼び出す必要があり、再入攻撃を回避します。

3. 明確な呼び出し失敗：実行時の失敗は、明確な失敗、ガスの枯渇、数量のオーバーフローの三つのケースのみであり、一般的な実行時攻撃を回避しています。

4. 厳密なセマンティクス：大文字と小文字、スペース、短い行などに厳格な規則があり、コード監査を容易にします。

これらの改善により、MichelsonはEthereum上で一般的な攻撃タイプに対してより良く耐えることができます。

!

SmartPy 開発キット

Tezos上のDApp開発者はMichelson言語を習得する必要はありません。彼らはPythonベースのSmartPy SDKを使用して、Pythonコードで書かれたスマートコントラクトをMichelson言語にコンパイルできます。したがって、DApp開発者はPythonを理解するだけで簡単に始めることができます。

SmartPyはPythonライブラリで、SmartPy.ioはユーザーがブラウザでPythonスクリプトを実行できるようにします。SmartPyの公式ウェブサイトではオンラインエディタが提供されており、開発者は直接Pythonでコードを書き、Michelsonスマートコントラクトにコンパイルし、その後Tezosメインネットにデプロイできます。その使用インターフェースはEthereumのRemixオンラインエディタよりもシンプルで明快であり、非常に使いやすいです。SmartPyにはいくつかの既成の開発テンプレートも付属しており、開発者が参考にして学ぶのに便利です。

SmartPy.ioのインターフェースには、コード作成エリアと実行結果表示エリアが含まれています。開発者はPythonを使用して簡単に契約コードを作成および編集できます。SmartPyはコンパイルと実行プロセスを簡素化しており、実行ボタンをクリックするだけで完了します。実行結果は画面の右側に即座に表示され、契約呼び出しエントリ、ストレージステータス、コンパイル後のMichelsonコードなどが含まれます。

オンラインエディタの他に、SmartPyはコマンドラインバージョンのSmartPyBasicも提供しており、開発者はローカル環境でSmartPyコードをコンパイルして実行できます。デプロイされたスマートコントラクトはSmartPy Contract Explorerを通じて確認でき、コントラクトの現在の状態と履歴操作が一目でわかります。

現在、SmartPyはPythonの多くの一般的な機能をサポートしています。例えば、ローカル変数、変数の型判定、Lambda関数などです。サポートされていない機能の一部（例えば、配列）はmapで代用できます。これは、SmartPyを学ぶために多くの時間や労力を投入する必要がなく、開発者はより優れた機能の実装に集中できることを意味しています。

SmartPyを始めたい開発者のために、参考にできるいくつかのトレーニングコースがあります：

1. クラフトバース・ウォーズ
2. Blockmatics SmartPy開発者コース

!