一般信息

Runtime Verification是一種計算系統分析和執行的方法，旨在從運行中的系統中提取信息，以檢測和可能響應觀察到的行爲是否滿足或違反某些屬性。這種技術可以用於多種目的，如安全或安全策略監控、調試、測試、驗證、驗證、性能分析、故障保護、行爲修改等。它通過分析少量執行軌跡並直接與實際系統工作，避免了傳統形式驗證技術的複雜性。

Runtime Verification Inc.是一家專注於使用運行時驗證技術進行虛擬機和智能合約安全審計的公司。他們提供的服務包括設計審查、代碼審查、審計和智能合約及協議的形式驗證。

Runtime Verification Inc. 目前提供哪些產品？

Runtime Verification Inc. 目前正在開發三個核心產品：RV-Predict 是一種預測性運行時分析工具，專注於自動檢測程序中的併發錯誤。RV-Monitor 是一種開發方法和庫生成工具，允許在運行時監控和執行用戶選擇的屬性。RV-Match 是一種工具，允許對所有可能的程序路徑以符號方式執行詳盡的運行時驗證，從而證明某些屬性對於給定程序的所有可能執行都是正確的。

何時以及爲何應使用 RV-Predict？

每當併發正確性對多線程應用程序很重要時，都應該使用 RV-Predict。RV-Predict 能夠高效、無縫地檢測程序中的併發問題和數據爭用，非常易於運行，並且通常不需要任何配置。RV-Predict 還利用獨特的預測功能來檢測可能的爭用，即使它們未發生在 RV-Predict 記錄的執行跟蹤中。

何時以及爲何應使用 RV-Monitor？

RV-Monitor 允許監控複雜的應用程序或系統，並對其執行跟蹤執行屬性。只要存在用於管理程序開發的規範，就應使用 RV-Monitor，並且遵守該規範是軟件的關鍵功能。RV-Monitor 還可用於監控對通用 API（包括 Android 和 Java API）的合規性。

何時以及爲何應使用 RV-Match？

RV-Monitor 可以驗證並強制符合給定程序執行的某些屬性，而 RV-Match 可以在運行時證明程序的正確性，從而分析所有可能的執行路徑和所有可能的輸入上的執行跟蹤。RV-Match 提供強大的正確性保證，利用目標語言的正式定義語義以符號方式模擬執行。當需要形式驗證的有力保證時，應使用 RV-Match，也可以與 RV-Monitor 一起使用，以消除可證明從未違反屬性的區域的監控。

Runtime Verification Inc. 的產品涵蓋哪些許可證？

RV 開發的項目分爲兩類：專有產品和根據開放許可證許可的項目（作爲 RV 開源生態系統的一部分）。

專有產品包括未根據開放許可證明確許可的所有產品，僅用於評估和學術/非商業目的。未經事先許可，不得使用專有 RV 產品創建衍生作品，並且 RV 保留對專有產品的所有權利。不得以任何方式對專有產品進行逆向工程。

區塊鏈項目審計

Runtime Verification已經參與了多個區塊鏈項目的審計工作，包括但不限於以下方面：

- 智能合約的安全審計：他們提供對ERC-20、ERC-721、ERC-4626等合約的低成本審計。

- 協議的安全審計：包括借貸相關操作的協議。

- 形式驗證：提供開源的形式驗證和開發者工具，以降低審計成本並實現持續的形式驗證。

他們的審計通常包括手動審查和形式驗證，確保代碼的高安全性和可靠性。