MetaTrust Labs gần đây đã hoàn thành xác minh chính thức đầu tiên của giao thức Uniswap V3 Swap theo yêu cầu từ Xcalibyte. Quá trình xác minh đã phân tích kỹ lưỡng mã nguồn của Uniswap và đã chứng minh về mặt toán học rằng nó thực hiện chính xác mô hình tài chính dự định được mô tả trong sách trắng Uniswap V3.

Để xác minh mô hình và mã phức tạp của Uniswap, MetaTrust Labs đã tận dụng một công cụ phân tích sáng tạo mà họ đã phát triển. Đây là cách xác minh đã được thực hiện theo nhóm.

Là một phần trong nghiên cứu của chúng tôi về bảo mật Web 3.0, chúng tôi đã tiến hành xác minh chính thức một phần lớn Uniswap V3.

Trước tiên, chúng tôi đã xây dựng một mô hình chính thức của mã nguồn Uniswap V3 bằng cách sử dụng ngôn ngữ đặc tả được hỗ trợ bởi công cụ xác minh của chúng tôi.

Thứ hai, chúng tôi đã cung cấp cho mô hình chính thức Uniswap các thuộc tính mà nó phải đáp ứng, sử dụng logic do công cụ của chúng tôi xác định. Các thuộc tính này chính thức hóa mô hình tài chính được mô tả trong sách trắng Uniswap V3, liên quan đến các khái niệm toán học phức tạp như tích phân rời rạc.

Do tính chất phức tạp của mô hình tài chính của Uniswap V3, các công cụ xác minh tiêu chuẩn không thể chứng minh mã Uniswap thể hiện chính xác mô hình toán học của nó. Công cụ của chúng tôi sử dụng các kỹ thuật xác minh tiên tiến và cơ chế mới để xác định và xác minh một hệ thống phức tạp như vậy.

Về mặt kỹ thuật, công cụ sử dụng Logic phân tách được tăng cường với Tinh chỉnh dữ liệu để cho phép xác minh tự động, tất cả được phát triển bằng cách sử dụng trình chứng minh định lý Isabelle/HOL. Việc sử dụng một trình chứng minh định lý đảm bảo bản thân công cụ này đã được chính thức hóa hoàn toàn về mặt toán học.

So với các phương pháp hiện có, đầu tiên, người chứng minh định lý cung cấp một cơ sở đáng tin cậy tối thiểu để xác minh ở trạng thái hiện đại. Thứ hai, logic được hình thức hóa trong một trình chứng minh định lý biểu cảm cho phép công cụ của chúng tôi chỉ định và xác minh các thuộc tính cấp cao của các mô hình tài chính, chẳng hạn như tích phân rời rạc được mô tả trong sách trắng Uniswap V3.

Thành công nêu bật giá trị của các công cụ xác minh tùy chỉnh trong việc kiểm tra các hệ thống DeFi tinh vi. Xác minh dựa trên cơ sở toán học đang cho phép thế hệ tiếp theo của DApps đáng tin cậy và được sử dụng rộng rãi.

David từ MetaTrust Lab cho biết: "Chúng tôi tự hào cung cấp các khả năng phân tích là công cụ để đạt được thành tựu quan trọng này. Việc xác minh chính thức ở cấp độ này đặt ra một tiêu chuẩn mới về tính minh bạch và độ tin cậy trong phần mềm chuỗi khối".

Lần xác minh chính thức đầu tiên của giao thức Uniswap V3 Swap là một bước đột phá cho hệ sinh thái DeFi và là mô hình cho sự hợp tác trong tương lai, đồng thời điều này đã mang lại cho người dùng Uniswap thêm lý do để tin tưởng và chấp nhận nền tảng của nó.