EthSystems xác minh hình thức Privacy Pools của Ethereum đến mã trên Sepolia

EthSystems đã hoàn tất xác minh hình thức từ tài liệu thiết kế Privacy Pools của Ethereum (ETH) đến mã chạy trên mạng thử nghiệm Sepolia. Quá trình này phát hiện 6 vấn đề, trong đó 3 vấn đề đến từ chính các công cụ xác minh.

PANews đưa tin EthSystems công bố kết quả vào ngày 27. Privacy Pools là công nghệ được thiết kế để che thông tin giao dịch, đồng thời kiểm tra giao dịch có tuân thủ các quy tắc đã định hay không. Đợt xác minh lần này rà soát từng bước xem nội dung trong tài liệu thiết kế có được phản ánh trong phần triển khai và mã đã triển khai hay không.

Xác minh hình thức là phương pháp biểu diễn bằng toán học các điều kiện mà chương trình phải đáp ứng, rồi dùng công cụ kiểm tra xem các điều kiện đó có được thỏa mãn hay không. EthSystems sử dụng Lean để xác minh mô hình, mạch và hàm băm; Halmos và Kontrol để xác minh hợp đồng thông minh; còn ví được kiểm tra bằng Aeneas và Verus.

Ở các bước xác minh và triển khai, nhóm tạo lại mã rồi đối chiếu từng byte với mã byte đang chạy trên mạng thử nghiệm Sepolia. Mã byte là phần mã mà mạng thực sự thực thi. Quy trình này giúp kiểm tra liệu kết quả rà soát tài liệu thiết kế và mã nguồn dễ đọc có được phản ánh trong mã đã triển khai hay không.

Hai mục tiêu xác minh trọng tâm là ngăn chi tiêu hai lần và bảo toàn giá trị. Các điều kiện này nhằm ngăn việc sử dụng cùng một tài sản hai lần hoặc làm tăng giá trị trong quá trình giao dịch mà không có căn cứ. EthSystems cho biết đã dùng bộ chứng minh định lý Lean để xác minh máy móc cả hai điều kiện.

Quá trình xác minh phát hiện 6 vấn đề, trong đó 3 vấn đề xuất phát từ công cụ xác minh. Trong thông báo, EthSystems không nêu chi tiết từng vấn đề hoặc cho biết chúng đã được khắc phục hay chưa.

Kết quả xác minh vẫn dựa trên một số giả định. PANews đưa tin EthSystems nêu các điều kiện làm cơ sở cho kết quả gồm không xảy ra va chạm hàm băm, từ chối bằng chứng giả mạo, và sự tương thích trong hoạt động giữa hợp đồng thông minh với mô hình xác minh. Vì vậy, cần hiểu kết quả trong phạm vi các điều kiện này được duy trì.

Để giải quyết vấn đề thông tin giao dịch bị công khai trên sổ cái công khai của Ethereum, EthSystems đang phát triển công nghệ bảo mật dành cho tổ chức. Thông báo lần này nêu phạm vi xác minh từ tài liệu thiết kế đến mã chạy trên mạng thử nghiệm, đồng thời công khai các giả định còn lại.