一般的な情報

ランタイム検証は、実行中のシステムから情報を抽出して、観察された動作が特定の属性を満たしているか違反しているかを検出し、応答するように設計されたシステム分析と実行を計算する方法です。この手法は、セキュリティまたはセキュリティポリシーの監視、デバッグ、テスト、検証、検証、パフォーマンス分析、障害保護、動作修正など、さまざまな目的で使用できます。少数の実行トラックを分析し、実際のシステムと直接連携することで、従来の形式の検証手法の複雑さを回避します。

ランタイム検証株式会社は、ランタイム検証手法を使用した仮想マシンおよびスマートコントラクトのセキュリティ監査に特化した企業です。彼らが提供するサービスには、設計レビュー、コードレビュー、監査、スマートコントラクトおよびプロトコルの形式検証が含まれます。

Runtime Verification Inc.は現在どのような製品を提供していますか?

Runtime Verification Inc.は現在、3つのコア製品を開発しています。RV-Predictは、プログラム内の同時エラーの自動検出に焦点を当てた予測ランタイム分析ツールです。RV-Monitorは、ユーザーが選択したプロパティを実行時に監視および実行できる開発手法およびライブラリ生成ツールです。RV-Matchは、特定のプロパティが特定のプログラムのすべての可能な実行に対して正しいことを証明するために、可能なすべてのプログラムパスに対して詳細な実行時検証を記号的に実行できるツールです。

RV-Predictをいつ、なぜ使用する必要がありますか?

マルチスレッドアプリケーションにとって並行性の正確性が重要な場合はいつでも、RV-Predictを使用する必要があります。RV-Predictは、プログラム内の並行性の問題やデータ競合を効率的かつシームレスに検出し、非常に簡単に実行でき、通常は構成を必要としません。RV-Predictはまた、RV-Predictレコードの実行トレースで発生していない場合でも、起こりうる競合を検出するための独自の予測機能を活用しています。

RV-Monitorは、いつ、なぜ使用する必要がありますか?

RV-Monitorを使用すると、複雑なアプリケーションやシステムを監視し、それらに対して実行属性のトレースを実行できます。RV-Monitorは、プログラム開発を管理するための仕様が存在する限り使用する必要があり、その仕様に準拠することがソフトウェアの重要な機能です。RV-Monitorは、AndroidやJava APIを含む一般的なAPIへの準拠を監視するためにも使用できます。

いつ、なぜRV-Matchを使用する必要がありますか?

RV-Monitorは、指定されたプログラムの実行に適合する特定のプロパティを検証および強制することができますが、RV-Matchは、実行時にプログラムの正しさを証明することにより、すべての可能な実行パスとすべての可能な入力の実行トレースを分析します。RV-Matchは、ターゲット言語の正式に定義されたセマンティクスを使用して、記号的に実行をシミュレートする強力な正確性保証を提供します。形式検証の強力な保証が必要な場合は、RV-Matchを使用するか、RV-Monitorと組み合わせて使用して、プロパティに違反し

Runtime Verification Inc.の製品はどのようなライセンスを対象としていますか?

RVによって開発されたプロジェクトは、プロプライエタリ製品とオープンライセンスに基づいてライセンスされたプロジェクトの2つに分類されます（RVオープンソースエコシステムの一部として）。

プロプライエタリ製品には、オープンライセンスに基づいて明示的にライセンスされていないすべての製品が含まれ、評価および学術/非営利目的のみに使用されます。事前の許可なしに、プロプライエタリRV製品を使用して派生作品を作成することはできず、RVはプロプライエタリ製品に関するすべての権利を留保します。プロプライエタ

ブロックチェーンプロジェクト監査

Runtime Verificationは、以下を含むがこれに限定されない複数のブロックチェーンプロジェクトの監査に参加しています。

-スマートコントラクトのセキュリティ監査: ERC-20、ERC-721、ERC-4626などの契約の低コスト監査を提供します。

-プロトコルのセキュリティ監査:借入関連の操作を含むプロトコル。

-形式検証:オープンソースの形式検証と開発者ツールを提供して、監査コストを削減し、継続的な形式検証を実現します。

彼らの監査には通常、手動レビューと形式検証が含まれ、コードの高い安全性と信頼性を確保しています。