セキュリティ、テスト、形式的検証

私たちは、重要なシステムの安全性と正確性を確保するための厳密なツールを構築している研究開発企業、Runtime Verificationです。私たちのチームは、K Frameworkで記述された、Ethereum Virtual Machine（EVM）の最も完全で実戦テスト済みの形式的セマンティクスであるKEVMを開発しました。 KEVMは単なる仕様ではなく、スマートコントラクトのシンボリックな推論、適合性テストの実行、ガス使用量の分析、プログラムのデバッグ、および正確性プロパティの形式的検証に使用できる実行可能な仕様です。Ethereumの完全なテストスイートに合格しており、SolidityとVyperの両方のERC-20トークンを含む、価値の高いコントラクトの検証に使用されています。最近、Pectraアップグレードをサポートするためにセマンティクスを更新しました。 KEVMは、Solidity向けの形式的検証ツールであるKontrolによって積極的に活用されています。Kontrolは、Optimism、Ethereum Foundation、Lido、UniswapなどのEVMエコシステムの主要チームや、より広範なEthereumコミュニティのセキュリティ研究者や監査人によって積極的に使用されています。 私たちはこのリポジトリを積極的に維持し、Ethereumのプロトコルの進化に貢献し、Foundryなどの開発者ツールと統合しています。KEVMを通じて、証明可能で安全なスマートコントラクトインフラストラクチャにおいて可能なことの限界を押し広げています。

Actは、形式的検証のためのスマートコントラクト仕様言語およびツールキットです。Actの仕様は、EVMプログラムの考えられるすべての動作を形式的かつ高レベルで記述したものです。Actを使用すると、既存の多くの汎用検証ツールを活用して、仕様に関する特性を証明できます。このようなツールには、SMTソルバー (cvc5、z3、bitwuzla)、定理証明器 (Coq)、および経済分析ツール (CheckMate、Open Games) が含まれます。Actの仕様は、EVMの具体的な実装と同等であることを自動的に証明できます。非常に単純なコントラクトの場合、EVMバイトコードからActの仕様を自動生成できます。 これは、EVMバイトコードの高レベルな特性に関する原則的な推論をサポートするエンドツーエンドのパイプラインです。正確性 (例: 会計の不変条件) と経済的特性 (例: インセンティブの互換性) の両方に関する推論をサポートします。Actの仕様は高レベルのスマートコントラクト表現として機能し、既存の汎用分析および検証ツールをEVMコンテキストに簡単に統合できるようにします。

Titanoboaは、Vyperスマートコントラクト向けの最新の統合開発エクスペリエンスを提供するVyperインタープリターおよびテストフレームワークです。これにより、開発者はPython内で直接Vyperコントラクトをテストおよびデバッグでき、見やすいトレースバック、フォーキング、デバッグ機能、pytest統合、および標準のファジングなどの機能を提供します。スタンドアロン機能を超えて、TitanoboaはApeやMoccasinなどの他の人気のあるテストフレームワークの基盤として機能し、Vyperエコシステムのインフラストラクチャのコアピースです。