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.

Act là một ngôn ngữ đặc tả smart contract và bộ công cụ dành cho formal verification (xác minh hình thức). Các đặc tả của Act là một mô tả hình thức, cấp cao về tất cả các hành vi có thể có của một chương trình EVM. Act cho phép tận dụng nhiều công cụ xác minh đa năng hiện có để chứng minh các thuộc tính về đặc tả. Các công cụ như vậy bao gồm SMT solvers (cvc5, z3, bitwuzla), theorem provers (Coq) và công cụ phân tích kinh tế (CheckMate, Open Games). Các đặc tả của Act có thể được tự động chứng minh là tương đương với các triển khai cụ thể trong EVM. Đối với các hợp đồng rất đơn giản, các đặc tả của Act có thể được tạo tự động từ EVM bytecode. Đây là một quy trình end-to-end hỗ trợ lập luận có nguyên tắc về các thuộc tính cấp cao của EVM bytecode. Nó hỗ trợ lập luận về cả tính đúng đắn (ví dụ: các bất biến kế toán) và các thuộc tính kinh tế (ví dụ: tính tương thích của các ưu đãi). Các đặc tả của Act đóng vai trò như một đại diện smart contract cấp cao, cho phép dễ dàng tích hợp các công cụ phân tích và xác minh đa năng hiện có vào bối cảnh EVM.

Titanoboa là một trình thông dịch và framework thử nghiệm Vyper cung cấp trải nghiệm phát triển hiện đại, tích hợp cho các hợp đồng thông minh Vyper. Nó cho phép các nhà phát triển kiểm tra và gỡ lỗi các hợp đồng Vyper trực tiếp trong Python, cung cấp các tính năng như traceback đẹp mắt, forking, khả năng gỡ lỗi, tích hợp pytest và fuzzing có sẵn. Ngoài các khả năng độc lập của nó, Titanoboa đóng vai trò là nền tảng cho các framework thử nghiệm phổ biến khác như Ape và Moccasin, và là một phần cơ sở hạ tầng cốt lõi cho hệ sinh thái Vyper.