Bảo mật, thử nghiệm & xác minh hình thức

Chúng tôi là Runtime Verification, một công ty nghiên cứu và phát triển xây dựng các công cụ nghiêm ngặt để đảm bảo tính an toàn và tính đúng đắn của các hệ thống quan trọng. Nhóm của chúng tôi đã phát triển KEVM, ngữ nghĩa hình thức hoàn chỉnh và được thử nghiệm thực tế nhất của Máy ảo Ethereum (EVM), được viết bằng K Framework. KEVM không chỉ là một đặc tả, nó là một đặc tả có thể thực thi được có thể được sử dụng để lập luận tượng trưng về các hợp đồng thông minh, chạy các bài kiểm tra sự phù hợp, phân tích việc sử dụng gas, gỡ lỗi chương trình và xác minh chính thức các thuộc tính đúng đắn. Nó vượt qua toàn bộ bộ thử nghiệm Ethereum và được sử dụng để xác minh các hợp đồng có giá trị cao, bao gồm các token ERC-20 trong cả Solidity và Vyper. Gần đây, chúng tôi đã cập nhật ngữ nghĩa để hỗ trợ bản nâng cấp Pectra. KEVM đang được sử dụng tích cực bởi Kontrol - công cụ xác minh hình thức của chúng tôi cho Solidity, được sử dụng tích cực bởi các nhóm hàng đầu trong hệ sinh thái EVM, bao gồm Optimism, Ethereum Foundation, Lido, Uniswap, cũng như các nhà nghiên cứu bảo mật và kiểm toán viên trên toàn cộng đồng Ethereum rộng lớn hơn. Chúng tôi tích cực duy trì kho lưu trữ này, đóng góp vào sự phát triển giao thức của Ethereum và tích hợp với các công cụ dành cho nhà phát triển như Foundry. Thông qua KEVM, chúng tôi đang vượt qua ranh giới của những gì có thể làm được trong cơ sở hạ tầng hợp đồng thông minh an toàn và đúng đắn có thể chứng minh được.

Một trình tạo bài kiểm tra smart contract dựa trên Kỹ thuật Cây phân nhánh (Branching Tree Technique).

Runtime Verification đã đi đầu trong các công cụ xác minh hình thức mã nguồn mở trong hơn một thập kỷ. Cách tiếp cận tổng quát của chúng tôi cho phép chúng tôi sử dụng công nghệ của mình trên nhiều blockchain. Trong khi KEVM cung cấp cơ sở hạ tầng xác minh của chúng tôi cho tất cả các hợp đồng thông minh dựa trên EVM, Kontrol làm giảm đáng kể rào cản gia nhập đối với việc xác minh hình thức cho các hợp đồng thông minh Solidity. Công cụ của chúng tôi hoàn toàn là mã nguồn mở và có thể truy cập miễn phí cho tất cả các nhà phát triển của hệ sinh thái Optimism mà không mất thêm chi phí. KEVM là một ngữ nghĩa hình thức có thể thực thi EVM được viết trong K framework. KEVM vượt qua tất cả các bài kiểm tra sự phù hợp của Ethereum và là điểm khởi đầu để xác minh chính thức các hợp đồng thông minh với K framework. Tuy nhiên, việc sử dụng KEVM thuần túy đòi hỏi phải đào tạo đặc biệt về K framework để viết các đặc tả. Ngoài ra, các đặc tả này có thể khá dài dòng, làm tăng độ khó khi viết chúng. Kontrol giải quyết vấn đề này bằng cách cho phép các nhà phát triển viết đặc tả hình thức cho các hợp đồng thông minh của họ trực tiếp dưới dạng các bài kiểm tra thuộc tính Foundry. Các bài kiểm tra này được tự động dịch sang các đặc tả KEVM, giữ nguyên tất cả các đảm bảo xác minh trong khi cho phép trải nghiệm nhà phát triển dễ dàng hơn nhiều.