VerX: スマートコントラクトの安全性検証

VerXを紹介します。これは、Ethereumスマートコントラクトの機能的性質を証明できる最初の自動検証器です。VerXは、すべての実世界の契約がカスタム機能仕様を満たす必要があるという重要な問題に取り組んでいます。VerXは、無限状態スマートコントラクトの時間的特性を自動的に検証するための3つの技術を慎重に組み合わせたものです：（i）時間的特性検証の到達可能性チェックへの還元、（ii）Ethereum契約の実用的断片に対して正確かつ効率的な新しいシンボリック実行エンジン、そして（iii）トランザクション中にシンボリック実行を使用し、トランザクション境界で抽象化を行う遅延述語抽象化です。83の時間的特性と、人気のあるクラウドセールやライブラリを含む12の実世界プロジェクトに対する広範な実験評価により、VerXが実際に効果的であることが示されました。