zkWasm được CertiK xác minh hình thức, loại trừ một số logic

Kết quả xác minh hình thức đối với các mạch cốt lõi của zkWasm do CertiK hoàn tất năm 2024 đang được chú ý trở lại. Tuy nhiên, đây không phải công trình mới hoàn tất năm 2026 mà là nội dung nghiên cứu trước đó được giới thiệu lại.

Trong một bài blog kỹ thuật năm 2024, CertiK cho biết đã xác minh rằng mạch Halo2 của zkWasm biểu thị trạng thái phù hợp với quy tắc thực thi WebAssembly (Wasm) khi đáp ứng các ràng buộc hợp lệ. Delphinus Lab, đơn vị phát triển, cũng công bố vào ngày 2 tháng 5 năm 2024 rằng triển khai zkWasm của họ đã được xác minh hình thức.

zkWasm là hệ thống tạo bằng chứng không kiến thức, cho phép xác nhận tính hợp lệ của kết quả mà không cần thực hiện lại toàn bộ quá trình tính toán sau khi chương trình Wasm chạy. Dấu vết thực thi chương trình được chuyển thành nhiều bảng của Halo2, còn bên xác minh kiểm tra liệu từng bảng có đáp ứng các ràng buộc số học đã định hay không.

Xác minh hình thức khác với kiểm toán mã nguồn thông thường. Quy trình này không chỉ tìm các mẫu lỗ hổng đã biết mà còn chuyển câu hỏi liệu chương trình có hoạt động theo các quy tắc được định nghĩa trong những điều kiện cụ thể hay không thành một mệnh đề toán học mà máy có thể kiểm tra.

Trong zkVM, một mạch có thể xử lý nhiều kiểu thực thi chương trình. Vì vậy, việc xác nhận các ràng buộc của mạch có khớp với ngữ nghĩa thực thi Wasm thực tế hay không là bước then chốt để đánh giá tính đúng đắn của kết quả chứng minh.

Kho lưu trữ công khai của CertiK cho biết hoạt động xác minh hình thức viết bằng Coq bao phủ các thành phần chính của mạch zkWasm, gồm bảng thực thi, bảng bộ nhớ, ngăn xếp gọi hàm và phép toán bit. Mục tiêu là chứng minh rằng khi mọi ràng buộc của mạch được đáp ứng, mỗi hàng trong dấu vết thực thi đều biểu thị trạng thái phù hợp với quy tắc thực thi Wasm.

Tài liệu công khai cũng cho biết các vấn đề trong hoạt động truy cập bộ nhớ và cấu trúc gọi·trả về của mạch đã được phát hiện và sửa chữa trong quá trình xác minh. Điều này cho thấy xác minh hình thức không chỉ dừng ở việc kiểm tra mã hiện có mà còn có thể phát hiện sự không nhất quán giữa đặc tả và triển khai.

Tuy nhiên, không nên diễn giải rằng 'toàn bộ zkWasm đã được xác minh hoàn toàn'. Kho lưu trữ công khai bao gồm mô hình Coq, mã chứng minh và quy trình biên dịch, nhưng toàn bộ thuật toán viết bằng Rust không nằm trong phạm vi xác minh.

Mức độ công khai cũng có giới hạn. Dù mã xác minh đã được công bố, một số cấu phần của mạch, logic giải mã lệnh, hoạt động của trình thông dịch Wasmi và Halo2 vẫn được giả định hoặc loại khỏi phạm vi xác minh.

Trình thông dịch Wasmi, bản thân Halo2 và một phần mã tạo ràng buộc cũng không nằm trong phạm vi xác minh. Chức năng gọi bên ngoài và một số logic giải mã lệnh tiếp tục phụ thuộc vào các giả định riêng hoặc đánh giá thủ công.

CertiK cho biết kho lưu trữ nội bộ tương ứng có tổng cộng 33.080 dòng mã Coq. Việc công khai quy mô mã không đồng nghĩa toàn bộ phạm vi chứng minh đã được công bố.

Báo cáo thường niên năm 2024 của CertiK cho biết đối tượng xác minh là mạch zkWasm gồm 144 lệnh, đồng thời đánh giá đây là hoạt động xác minh hình thức hoàn chỉnh đầu tiên trong hệ sinh thái bằng chứng không kiến thức. Đây là mô tả của CertiK, còn tiêu chuẩn so sánh độc lập hoặc kết quả đánh giá đồng cấp chưa thể được xác nhận từ các tài liệu công khai.

CertiK cho biết khung xác minh hình thức này có thể được áp dụng cho các zkVM và zkEVM khác. Tuy nhiên, đây chỉ là nhận định của công ty về khả năng ứng dụng, không có nghĩa hoạt động xác minh đối với các hệ thống khác đã hoàn tất.

Delphinus Lab đã chia sẻ thông tin về việc triển khai zkWasm của mình được xác minh hình thức và đính kèm tài liệu kỹ thuật của CertiK. Phản hồi tích cực từ phía đơn vị phát triển đã được ghi nhận, nhưng điều đó không đồng nghĩa phạm vi xác minh đã mở rộng sang toàn bộ ngăn xếp phần mềm.

CertiK sau đó giới thiệu việc dùng Verus để tái triển khai một phần bằng chứng zkWasm trước đây, đồng thời giảm quy mô mã từ 2.440 dòng xuống còn 595 dòng. Đây là nghiên cứu tiếp theo, tách biệt với công bố hoàn tất xác minh ban đầu, và không nên được xem là kết quả mở rộng phạm vi công khai của hoạt động xác minh trước đó.

Nghiên cứu liên quan đã được đăng ký trong chương trình ACM CCS 2026 dưới dạng bài báo dự kiến công bố với tiêu đề 'Formal Verification of Circuit-Soundness in zkWasm, a General Purpose zkVM'. Nhóm nghiên cứu gồm các nhà nghiên cứu từ CertiK, Delphinus Lab, NVIDIA, Đại học Columbia và Đại học Yale. Toàn văn bài báo và chi tiết kết quả phản biện chưa thể được xác nhận chỉ từ các tài liệu công khai.

Điểm đáng chú ý của trường hợp này là nỗ lực giải thích tính chính xác của mạch trong hạ tầng zkVM bằng phương pháp toán học đã tạo ra một kết quả nghiên cứu cụ thể. Đồng thời, cần phân biệt rõ phạm vi xác minh và khả năng tái lập đã được công khai với tính an toàn của toàn bộ phần mềm.