Thông tin chung
Runtime Verification là một phương pháp phân tích và thực thi hệ thống tính toán được thiết kế để trích xuất thông tin từ các hệ thống đang chạy để phát hiện và có thể phản ứng với các hành vi quan sát được đáp ứng hoặc vi phạm các thuộc tính nhất định. Công nghệ này có thể được sử dụng cho nhiều mục đích như giám sát chính sách bảo mật hoặc bảo mật, gỡ lỗi, kiểm tra, xác minh, xác minh, phân tích hiệu suất, bảo vệ lỗi, sửa đổi hành vi, v.v. Nó tránh sự phức tạp của các kỹ thuật xác minh hình thức truyền thống bằng cách phân tích một lượng nhỏ quỹ đạo thực thi và làm việc trực tiếp với các hệ thống thực tế.
Runtime Verification Inc. là một công ty tập trung vào việc sử dụng công nghệ xác minh thời gian Các dịch vụ mà họ cung cấp bao gồm đánh giá thiết kế, đánh giá mã, kiểm toán và xác minh chính thức các hợp đồng và giao thức thông minh.
Runtime Verification Inc. Hiện đang cung cấp những sản phẩm nào?
Runtime Verification Inc. Hiện đang phát triển ba sản phẩm cốt lõi: Rv-Predict là một công cụ phân tích thời gian chạy dự đoán tập trung vào việc tự động phát hiện các lỗi đồng thời trong các chương trình. Rv-Monitor là một phương pháp phát triển và công cụ tạo thư viện cho phép giám sát và thực hiện các thuộc tính do người dùng chọn trong thời gian chạy. Rv-Match là một công cụ cho phép thực hiện xác nhận thời gian chạy chi tiết trên tất cả các đường dẫn chương trình có thể có, chứng minh rằng một số thuộc tính nhất định là chính xác cho tất cả các lần thực hiện có thể của một chương trình nhất định.
Khi nào và tại sao bạn nên sử dụng Rv-Predict?
Rv-Predict nên được sử dụng bất cứ khi nào tính chính xác đồng thời là quan trọng đối với các ứng dụng đa luồng. Rv-Predict có thể phát hiện hiệu quả và liền mạch các vấn đề đồng thời và tranh chấp dữ liệu trong các chương trình, rất dễ chạy và thường không yêu cầu bất kỳ cấu hình nào. Rv-Predict cũng sử dụng các tính năng dự đoán độc đáo để phát hiện các tranh chấp có thể xảy ra, ngay cả khi chúng không xảy ra trong quá trình theo dõi thực thi của các bản ghi Rv-Predict.
Khi nào và tại sao bạn nên sử dụng Rv-Monitor?
Rv-Monitor cho phép giám sát các ứng dụng hoặc hệ thống phức tạp và thực hiện các thuộc tính thực thi theo dõi trên chúng. Rv-Monitor nên được sử dụng bất cứ khi nào có thông số kỹ thuật để quản lý phát triển chương trình và tuân thủ thông số kỹ thuật này là một tính năng chính của phần mềm. Rv-Monitor cũng có thể được sử dụng để giám sát việc tuân thủ các API chung (bao gồm Android và API).
Khi nào và tại sao bạn nên sử dụng Rv-Match?
Rv-Monitor có thể xác minh và thực thi sự phù hợp với một số thuộc tính nhất định được thực hiện bởi một chương trình nhất định, trong khi Rv-Match có thể chứng minh tính đúng của chương trình tại thời gian chạy, do đó phân tích tất cả các đường dẫn thực thi có thể và theo dõi thực thi trên tất cả các đầu vào có thể. Rv-Match cung cấp đảm bảo tính đúng đắn mạnh mẽ, mô phỏng thực thi theo cách tượng trưng bằng cách sử dụng ngữ nghĩa được xác định chính thức của ngôn ngữ đích. Khi cần xác minh chính thức, Rv-Match nên được sử dụng, cũng có thể được sử dụng cùng với Rv-Monitor để loại bỏ
Các sản phẩm của Runtime Verification Inc. bao gồm những giấy phép nào?
Các dự án được phát triển bởi RV được chia thành hai loại: các sản phẩm độc quyền và các dự án được cấp phép theo giấy phép mở (như một phần của hệ sinh thái nguồn mở RV).
Các sản phẩm độc quyền bao gồm tất cả các sản phẩm không được cấp phép rõ ràng theo giấy phép mở và chỉ dành cho mục đích đánh giá và học thuật / phi thương mại. Không có tác phẩm phái sinh nào có thể được tạo ra bằng cách sử dụng các sản phẩm RV độc quyền mà không có sự cho phép trước và RV giữ lại tất cả các quyền đối với các sản phẩm độc quyền. Các sản phẩm độc quyền không được thiết kế ngược theo bất kỳ cách
Kiểm toán dự án blockchain
Runtime Verification đã tham gia vào việc kiểm toán nhiều dự án blockchain, bao gồm nhưng không giới hạn ở các khía cạnh sau:
- Kiểm toán bảo mật của hợp đồng thông minh: Họ cung cấp kiểm toán chi phí thấp cho các hợp đồng như ERC-20, ERC-721, ERC-4626.
- Kiểm toán bảo mật của giao thức: Giao thức bao gồm các hoạt động liên quan đến vay và cho vay.
- Xác minh chính thức: Cung cấp xác minh chính thức nguồn mở và các công cụ dành cho nhà phát triển để giảm chi phí kiểm toán và cho phép xác minh chính thức liên tục.
Kiểm toán của họ thường bao gồm đánh giá thủ công và xác minh chính thức, đảm bảo tính bảo mật và độ tin cậy cao của mã.
