Xác minh chính thức nâng cao về bằng chứng không có kiến ​​thức: cách xác minh lệnh ZK

Nguồn: Cộng đồng người Trung Quốc CertiK

Để hiểu sâu sắc cách áp dụng công nghệ xác minh chính thức cho zkVM (máy ảo không kiến ​​thức), bài viết này sẽ tập trung về việc xác minh một lệnh đơn. Để biết tình hình chung về xác minh chính thức nâng cao của ZKP (bằng chứng không có kiến ​​thức), vui lòng tham khảo bài viết "Xác minh chính thức nâng cao của Blockchain bằng chứng không có kiến ​​thức" mà chúng tôi đã xuất bản cùng lúc.

Xác minh hướng dẫn ZK là gì?

zkVM (máy ảo không kiến ​​thức) có thể tạo các đối tượng chứng minh ngắn làm bằng chứng cho thấy một chương trình cụ thể có thể chạy trên một số đầu vào nhất định và kết thúc thành công. Trong trường Web3.0, ứng dụng zkVM làm cho thông lượng cao hơn vì nút L1 chỉ cần xác minh bằng chứng ngắn gọn về quá trình chuyển đổi của hợp đồng thông minh từ trạng thái đầu vào sang trạng thái đầu ra và việc thực thi mã hợp đồng thực tế có thể được hoàn thành ngoài chuỗi .

Đầu tiên, trình chuẩn zkVM chạy chương trình để tạo bản ghi thực thi của từng bước, sau đó chuyển đổi dữ liệu bản ghi thực thi thành một tập hợp các bảng số (quá trình này được gọi là "số học hóa"). Các số này phải đáp ứng một tập hợp các ràng buộc (tức là các mạch), bao gồm các phương trình kết nối giữa các ô trong bảng cụ thể, các hằng số cố định, các ràng buộc tìm kiếm cơ sở dữ liệu giữa các bảng và các ràng buộc cần được thỏa mãn giữa mỗi cặp hàng của bảng liền kề. phương trình (còn gọi là "cổng"). Xác minh trên chuỗi có thể xác nhận rằng thực sự có một bảng đáp ứng tất cả các ràng buộc, đồng thời đảm bảo rằng sẽ không nhìn thấy các con số cụ thể trong bảng.

Việc thực thi từng lệnh VM phải đối mặt với nhiều ràng buộc như vậy. Ở đây chúng tôi gọi tập hợp các ràng buộc này của lệnh VM là "lệnh ZK" của nó. Dưới đây là ví dụ về ràng buộc lệnh tải bộ nhớ zkWasm được viết bằng Rust.

Việc xác minh chính thức các hướng dẫn ZK được thực hiện bằng cách thực hiện lý luận chính thức trên các mã này, trước tiên chúng tôi dịch sang ngôn ngữ chính thức.

Ngay cả khi chỉ có một ràng buộc duy nhất có lỗi, kẻ tấn công vẫn có thể gửi bằng chứng ZK độc hại. Bảng dữ liệu tương ứng với bằng chứng độc hại không tương ứng với hoạt động pháp lý của hợp đồng thông minh. Không giống như các chuỗi không phải ZK như Ethereum, có nhiều nút chạy các triển khai EVM (Máy ảo Ethereum) khác nhau, khiến cho cùng một lỗi khó có thể xảy ra cùng một lúc và ở cùng một vị trí, chuỗi zkVM chỉ có một VM duy nhất thực hiện. Chỉ xét từ góc độ này, chuỗi ZK dễ vỡ hơn hệ thống Web3.0 truyền thống.

Điều tệ hơn là, không giống như các chuỗi không phải ZK, do chi tiết tính toán của các giao dịch zkVM không được gửi và lưu trữ trên chuỗi nên sau khi cuộc tấn công xảy ra, việc khám phá các chi tiết cụ thể không chỉ rất khó khăn của cuộc tấn công, ngay cả việc xác định bản thân cuộc tấn công cũng có thể trở nên cực kỳ khó khăn.

Hệ thống zkVM yêu cầu kiểm tra cực kỳ nghiêm ngặt. Thật không may, tính chính xác của mạch zkVM rất khó đảm bảo.

Tại sao việc xác minh hướng dẫn ZK lại khó khăn?

VM (máy ảo) là một trong những phần phức tạp nhất của kiến ​​trúc hệ thống Web3.0. Các chức năng mạnh mẽ của hợp đồng thông minh là cốt lõi của việc hỗ trợ các khả năng của Web3.0. Sức mạnh của chúng đến từ các máy ảo cơ bản, vừa linh hoạt vừa phức tạp: để hoàn thành các tác vụ lưu trữ và tính toán chung, các máy ảo này phải có khả năng hỗ trợ nhiều hướng dẫn. và các tiểu bang. Ví dụ: việc triển khai geth của EVM yêu cầu hơn 7.500 dòng mã ngôn ngữ Go. Tương tự, mạch ZK hạn chế việc thực hiện các lệnh này cũng lớn và phức tạp. Giống như trong dự án zkWasm, việc triển khai mạch ZK cần hơn 6.000 dòng mã Rust.

Kiến trúc mạch zkWasm

Mạch zkVM có kích thước lớn hơn các mạch ZK chuyên dụng được sử dụng trong các hệ thống ZK được thiết kế cho các ứng dụng cụ thể như thanh toán cá nhân Hơn nữa: số lượng của các quy tắc ràng buộc có thể lớn hơn một hoặc hai bậc và các bảng số học có thể bao gồm hàng trăm cột với hàng triệu ô số.

Việc xác minh hướng dẫn ZK có ý nghĩa gì?

Ở đây chúng tôi muốn xác minh tính chính xác của lệnh XOR trong zkWasm. Về mặt kỹ thuật, bảng thực thi của zkWasm tương ứng với trình tự thực thi Wasm VM hợp pháp. Vì vậy, từ góc độ vĩ mô, điều chúng tôi muốn xác minh là mỗi khi lệnh này được thực thi, một trạng thái zkVM hợp pháp mới sẽ luôn được tạo: mỗi hàng trong bảng tương ứng với một trạng thái pháp lý của VM và hàng sau sẽ luôn Nó được tạo bằng cách thực hiện các hướng dẫn VM tương ứng. Hình dưới đây thể hiện định lý hình thức về tính đúng đắn của lệnh XOR.

Ở đây "state_rel i st" cho biết trạng thái "st" là trạng thái zkVM hợp pháp của hợp đồng thông minh ở bước "i". Như bạn có thể đoán, việc chứng minh "state_rel (i+1) ..." không hề đơn giản.

Làm cách nào để xác minh hướng dẫn ZK?

Mặc dù ngữ nghĩa tính toán của việc Lấy hai số nguyên từ bộ nhớ ngăn xếp, thực hiện phép tính XOR và sau đó lưu số nguyên mới được tính toán trở lại cùng một ngăn xếp. Ngoài ra, các bước thực hiện của hướng dẫn này phải được tích hợp vào toàn bộ quy trình thực hiện hợp đồng thông minh và thứ tự cũng như thời gian thực hiện phải chính xác.

Do đó, Hiệu quả thực thi của lệnh XOR là lấy hai số từ ngăn xếp dữ liệu, đẩy kết quả XOR của chúng, đồng thời tăng bộ đếm chương trình để trỏ đến lệnh tiếp theo của hợp đồng thông minh.

Không xấu Hóa ra, định nghĩa về các thuộc tính chính xác ở đây nhìn chung rất giống với những gì chúng ta gặp phải khi xác minh các máy ảo mã byte truyền thống (chẳng hạn như trình thông dịch EVM trong các nút Ethereum L1). Nó dựa trên định nghĩa trừu tượng cấp cao về trạng thái máy (ở đây là bộ nhớ ngăn xếp và luồng thực thi) và định nghĩa về hành vi dự kiến ​​của từng lệnh (ở đây là logic số học).

Tuy nhiên, như chúng ta sẽ thấy bên dưới, do đặc thù của ZKP và zkVM, quy trình xác minh tính chính xác của chúng thường rất khác so với quy trình xác minh tính chính xác của các máy ảo thông thường. Chỉ để xác minh hướng dẫn duy nhất của chúng tôi ở đây phụ thuộc vào tính chính xác của nhiều bảng trong zkWASM: trong số đó có bảng phạm vi được sử dụng để giới hạn kích thước của giá trị, bảng bit được sử dụng cho kết quả trung gian của phép tính bit nhị phân, Bảng thực thi lưu trữ trạng thái VM có kích thước không đổi trên mỗi hàng (tương tự như dữ liệu trong các thanh ghi và chốt trong CPU vật lý) và bộ nhớ đại diện cho các bảng và bảng nhảy trạng thái VM có kích thước thay đổi linh hoạt (bộ nhớ, ngăn xếp dữ liệu và ngăn xếp cuộc gọi).

Bước 1: Bộ nhớ ngăn xếp

Tương tự như VM truyền thống, chúng ta cần đảm bảo rằng hai tham số nguyên của lệnh có thể được đọc từ ngăn xếp và các giá trị kết quả XOR của chúng ​​chính xác Ghi lại vào ngăn xếp. Cách biểu diễn chính thức của ngăn xếp cũng trông khá quen thuộc (cũng có bộ nhớ chung và bộ nhớ heap, nhưng lệnh XOR không sử dụng chúng).

zkVM sử dụng một sơ đồ phức tạp để biểu diễn dữ liệu động vì bộ chuẩn ZK không hỗ trợ các cấu trúc dữ liệu như ngăn xếp hoặc mảng. Ngược lại, đối với mỗi giá trị được đẩy vào ngăn xếp, bảng bộ nhớ ghi lại một hàng riêng biệt và một số cột được sử dụng để biểu thị thời gian hiệu lực của mục nhập. Tất nhiên, dữ liệu trong các bảng này có thể bị kẻ tấn công kiểm soát, do đó, một số ràng buộc phải được áp đặt để đảm bảo rằng các mục trong bảng thực sự tương ứng với các hướng dẫn ngăn xếp thực tế khi thực hiện hợp đồng. Điều này đạt được bằng cách tính toán cẩn thận số lần đẩy ngăn xếp trong quá trình thực hiện chương trình. Khi xác minh từng lệnh, chúng ta cần đảm bảo rằng số đếm này luôn chính xác. Ngoài ra, chúng tôi có một loạt bổ đề liên quan đến các ràng buộc được tạo bởi một lệnh duy nhất với việc tra cứu bảng và kiểm tra phạm vi thời gian thực hiện các hoạt động ngăn xếp. Từ cấp cao nhất, các ràng buộc đếm cho các hoạt động bộ nhớ được xác định như sau.

Bước 2: Các phép toán số học

Tương tự như VM truyền thống, chúng tôi muốn đảm bảo rằng phép toán XOR theo bit là chính xác. Xét cho cùng, điều này có vẻ dễ dàng, CPU máy tính vật lý của chúng ta có thể hoàn thành thao tác này chỉ trong một lần.

Nhưng đối với zkVM, việc này thực sự không hề đơn giản. Các hướng dẫn số học duy nhất được bộ chuẩn ZK hỗ trợ nguyên bản là phép cộng và phép nhân. Để thực hiện các thao tác bit nhị phân, VM sử dụng một sơ đồ khá phức tạp, trong đó một bảng lưu trữ các kết quả thao tác ở mức byte cố định và bảng còn lại hoạt động như một "bảng ghi chú" để hiển thị cách thực hiện các thao tác trên nhiều hàng của bảng. Số 64 bit được chia thành 8 byte rồi ghép lại để cho ra kết quả.

Đoạn của đặc tả bitmap zkWasm

Rất đơn giản trong các ngôn ngữ lập trình truyền thống Thao tác XOR, ở đây cần có nhiều bổ đề để xác minh tính đúng đắn của các bảng phụ trợ này. Đối với chỉ thị của chúng tôi, chúng tôi có:

Bước 3: Luồng thực thi

Tương tự như VM truyền thống, chúng ta cần đảm bảo rằng giá trị của bộ đếm chương trình được cập nhật chính xác. Đối với các lệnh tuần tự như XOR, bộ đếm chương trình cần được tăng lên một đơn vị sau mỗi bước.

Vì zkWasm được thiết kế để chạy mã Wasm nên cũng cần phải đảm bảo rằng tính chất bất biến của bộ nhớ Wasm được duy trì trong suốt quá trình thực thi.

Các ngôn ngữ lập trình truyền thống có hỗ trợ riêng cho các kiểu dữ liệu như giá trị Boolean, số nguyên 8 bit và số nguyên 64 bit. Tuy nhiên, trong mạch ZK, các biến luôn nằm trong phạm vi số nguyên modulo lớn. số nguyên tố (≈ 2254). Vì máy ảo thường chạy ở 64 bit nên các nhà phát triển mạch cần sử dụng hệ thống ràng buộc để đảm bảo chúng có phạm vi số chính xác và các kỹ sư xác minh chính thức cần theo dõi các thuộc tính bất biến về các phạm vi này trong suốt quá trình xác minh. Lý giải về các luồng thực thi và các bảng thực thi liên quan đến tất cả các bảng phụ trợ khác, vì vậy chúng ta cần kiểm tra xem phạm vi của tất cả dữ liệu bảng có chính xác hay không.

Tương tự như trường hợp quản lý số hiệu hoạt động của bộ nhớ, zkVM yêu cầu một bộ bổ đề tương tự để xác minh luồng điều khiển. Cụ thể, mỗi lệnh gọi và trả lại yêu cầu sử dụng ngăn xếp cuộc gọi. Ngăn xếp cuộc gọi được triển khai bằng cách sử dụng sơ đồ bảng tương tự như ngăn xếp dữ liệu. Đối với lệnh XOR, chúng ta không cần sửa đổi ngăn xếp cuộc gọi nhưng khi xác minh toàn bộ lệnh, chúng ta vẫn cần theo dõi và xác minh xem số lượng thao tác của luồng điều khiển có chính xác hay không.

Xác minh hướng dẫn này

Hãy tập hợp tất cả các bước lại với nhau và xác minh định lý tính đúng đắn từ đầu đến cuối của lệnh zkWasm XOR. Các xác minh sau đây được hoàn thành trong môi trường bằng chứng tương tác, trong đó mọi bước xây dựng chính thức và lý luận logic đều trải qua quá trình kiểm tra máy nghiêm ngặt nhất.

Như đã thấy ở trên, việc xác minh chính thức các mạch zkVM là khả thi. Nhưng đây là một nhiệm vụ khó khăn đòi hỏi sự hiểu biết và theo dõi nhiều tính chất bất biến phức tạp. Điều này phản ánh sự phức tạp của phần mềm đang được xác minh: mọi bổ đề liên quan đến việc xác minh cần phải được nhà phát triển mạch xử lý chính xác. Với mức độ rủi ro cao, sẽ rất có giá trị nếu chúng được kiểm tra bằng máy bằng hệ thống xác minh chính thức, thay vì chỉ dựa vào sự xem xét cẩn thận của con người.