Jolt zkVM xác minh 60/67 mã byte RISC-V, còn 7 lệnh chưa được kiểm chứng

LayerZero Research đã xác minh 60 trong số 67 phần mở rộng mã byte RISC-V của Jolt zkVM. Bảy lệnh còn lại vẫn nằm trong diện cần kiểm chứng do liên quan đến các trường hợp biên cụ thể.

CryptoBriefing đưa tin LayerZero Research đã thực hiện quá trình này trong khoảng hai tháng rưỡi, sử dụng trình trợ lý chứng minh định lý Lean. Tuy nhiên, các số liệu và bài nghiên cứu về quá trình xác minh chưa được xác nhận với cùng nội dung trên các kênh chính thức của LayerZero.

Kiểm chứng hình thức là phương pháp xác nhận phần mềm đáp ứng đặc tả định trước bằng chứng minh toán học, thay vì chỉ kiểm thử. Trong zkVM, nếu một lệnh bị diễn giải sai hoặc xảy ra lỗi trong quá trình thực thi, kết quả không chính xác có thể bị xử lý như một bằng chứng hợp lệ, khiến bước này có ý nghĩa quan trọng.

Phần mở rộng mã byte của Jolt giải mã các lệnh RISC-V nguyên bản trong tệp ELF, sau đó chuyển chúng thành biểu diễn nội bộ bao gồm toán hạng, địa chỉ, cờ mạch và cờ tra cứu. Tài liệu chính thức của Jolt mô tả mã byte là điểm tham chiếu của chương trình được thực thi.

Chỉ mục mã byte mở rộng và địa chỉ bộ nhớ ELF đảm nhiệm các vai trò khác nhau. Chỉ mục mã byte được dùng để truy cập lệnh trong chu kỳ thực thi, còn địa chỉ bộ nhớ ELF được sử dụng để kiểm tra các ràng buộc của bộ đếm chương trình.

Trong quá trình thực thi, hệ thống cũng chứng minh rằng lệnh được đọc trùng khớp với mã byte đã qua tiền xử lý. Vì vậy, độ chính xác của bước mở rộng mã byte có thể ảnh hưởng đến độ tin cậy của dấu vết thực thi và kết quả chứng minh sau đó.

Tuy nhiên, việc xác minh lần này không đồng nghĩa toàn bộ Jolt đã hoàn tất kiểm chứng hình thức. Andreessen Horowitz từng giải thích trong một bài viết kỹ thuật năm 2024 rằng công việc xác minh Jolt là quá trình từng bước kiểm tra tính nhất quán giữa ngữ nghĩa tra cứu, bằng chứng tương tác đa thức, hệ thống ràng buộc, đặc tả RISC-V và mã triển khai Rust thực tế.

Lộ trình xác minh do Andreessen Horowitz công bố cũng xem việc kiểm tra sự thống nhất giữa mô hình hình thức và mã triển khai thực tế là một nhiệm vụ riêng. Điều này có nghĩa mô hình hình thức được chứng minh trong Lean vẫn cần được đối chiếu thêm để xác nhận mô hình phản ánh chính xác triển khai thực tế.

Các nghiên cứu trước đây đã sử dụng trình trợ lý chứng minh định lý ACL2 để xác minh ngữ nghĩa tra cứu đối với các lệnh RISC-V RV32I của Jolt. Nhóm nghiên cứu kiểm tra việc phân rã lệnh thành các bảng tra cứu nhỏ có phù hợp với đặc tả RISC-V hay không, đồng thời phát hiện một số tối ưu hóa giúp giảm các lượt tra cứu không cần thiết.

Một nghiên cứu liên quan cho biết toàn bộ lệnh RV32I đã được hình thức hóa và xác minh bằng ACL2. Công việc dựa trên Lean lần này có thể được xem là một trường hợp kiểm tra phạm vi mở rộng mã byte bằng một trình trợ lý chứng minh định lý khác với nghiên cứu trước đó.

LayerZero giải thích trong tài liệu kỹ thuật về Zero rằng Jolt được sử dụng làm hạ tầng chứng minh thực thi của mạng lưới. Logic thực thi của Zero trải qua quy trình tạo và xác minh bằng chứng, trong đó Jolt đảm nhiệm vai trò zkVM chứng minh kết quả thực thi chương trình là chính xác.

Dù vậy, việc xác minh phần mở rộng mã byte không đủ để kết luận toàn bộ mạng Zero hoặc toàn bộ Jolt đã được xác minh về mặt bảo mật. Mức độ thống nhất giữa mã Rust thực tế và mô hình hình thức, cũng như phạm vi kiểm chứng của các thành phần chứng minh khác, vẫn cần được đánh giá riêng.

Các công bố kỹ thuật trước đây của LayerZero và Andreessen Horowitz về Akita và Lattice Jolt tập trung vào các thành phần mật mã của hạ tầng chứng minh không tri thức. Công việc lần này khác với những công bố đó khi tập trung vào cách diễn giải lệnh và chuyển đổi mã byte trong quá trình thực thi, thay vì phương thức cam kết đa thức.

Danh sách cụ thể của 60 lệnh đã được xác minh và 7 lệnh chưa được xác minh chưa được công bố. Đặc biệt, cần có thêm tài liệu để xác định 7 lệnh này liên quan đến những trường hợp biên nào và mã triển khai thực tế thống nhất với mô hình hình thức ở mức độ ra sao.

Có thể xem công bố lần này là tiến triển trong kiểm chứng hình thức đối với một thành phần cụ thể của Jolt zkVM. Tuy nhiên, phạm vi xác minh hiện còn giới hạn và không nên được diễn giải rộng thành việc hoàn tất kiểm chứng bảo mật của toàn bộ zkVM hoặc mạng Zero.