Phân tích nguyên lý Binius STARKs và những suy nghĩ tối ưu hóa

1 Giới thiệu

Một lý do chính dẫn đến hiệu suất thấp của STARKs là: hầu hết các giá trị trong chương trình thực tế đều khá nhỏ, chẳng hạn như chỉ số trong vòng lặp for, giá trị đúng sai, bộ đếm, v.v. Tuy nhiên, để đảm bảo tính an toàn của chứng minh dựa trên cây Merkle, việc sử dụng mã Reed-Solomon để mở rộng dữ liệu sẽ tạo ra nhiều giá trị dư thừa chiếm toàn bộ miền, ngay cả khi giá trị gốc rất nhỏ. Để giải quyết vấn đề này, việc giảm kích thước miền đã trở thành chiến lược then chốt.

Độ rộng mã của STARKs thế hệ đầu tiên là 252bit, độ rộng mã của STARKs thế hệ thứ hai là 64bit, độ rộng mã của STARKs thế hệ thứ ba là 32bit, nhưng độ rộng mã 32bit vẫn tồn tại nhiều không gian lãng phí. So với đó, miền nhị phân cho phép thao tác trực tiếp trên bit, mã hóa chặt chẽ hiệu quả và không có không gian lãng phí nào, tức là STARKs thế hệ thứ tư.

So với Goldilocks, BabyBear, Mersenne31 và các nghiên cứu gần đây về miền hữu hạn, nghiên cứu về miền nhị phân có thể được truy nguyên về những năm 1980. Hiện nay, miền nhị phân đã được ứng dụng rộng rãi trong mật mã, ví dụ điển hình bao gồm:

• Tiêu chuẩn mã hóa nâng cao (AES), dựa trên miền F28;

• Mã xác thực tin nhắn Galois ( GMAC ), dựa trên miền F2128;

• Mã QR, sử dụng mã hóa Reed-Solomon dựa trên F28;

• Giao thức FRI gốc và zk-STARK, cùng với hàm băm Grøstl vào vòng chung kết SHA-3, hàm này dựa trên miền F28, là một thuật toán băm rất thích hợp cho đệ quy.

Khi sử dụng miền nhỏ hơn, thao tác mở rộng miền trở nên ngày càng quan trọng để đảm bảo an toàn. Miền nhị phân mà Binius sử dụng hoàn toàn phụ thuộc vào việc mở rộng miền để đảm bảo an toàn và tính khả dụng thực tế. Hầu hết các đa thức liên quan đến tính toán Prover không cần phải vào miền mở rộng, mà chỉ cần hoạt động trong miền cơ sở, từ đó đạt được hiệu suất cao trong miền nhỏ. Tuy nhiên, kiểm tra điểm ngẫu nhiên và tính toán FRI vẫn cần phải đi sâu vào miền mở rộng lớn hơn để đảm bảo an toàn cần thiết.

Khi xây dựng hệ thống chứng minh dựa trên miền nhị phân, có 2 vấn đề thực tế: Khi tính toán biểu diễn trace trong STARKs, kích thước miền sử dụng phải lớn hơn bậc của đa thức; Khi cam kết Merkle tree trong STARKs, cần thực hiện mã hóa Reed-Solomon, kích thước miền sử dụng phải lớn hơn kích thước sau khi mở rộng mã.

Binius đã đề xuất một giải pháp đổi mới để xử lý hai vấn đề này, và đạt được điều đó bằng cách biểu thị cùng một dữ liệu theo hai cách khác nhau: đầu tiên, sử dụng đa biến ( cụ thể là đa thức đa tuyến tính ) thay thế cho đa thức đơn biến, thông qua các giá trị của nó trên "siêu khối" ( hypercubes ) để biểu thị toàn bộ quỹ đạo tính toán; thứ hai, do mỗi chiều của siêu khối có độ dài là 2, vì vậy không thể mở rộng Reed-Solomon tiêu chuẩn như STARKs, nhưng có thể coi siêu khối như là hình vuông ( square ), dựa trên hình vuông đó để thực hiện mở rộng Reed-Solomon. Phương pháp này đảm bảo an toàn trong khi tăng cường đáng kể hiệu quả mã hóa và hiệu suất tính toán.

2 Phân tích nguyên lý

Hiện tại, hầu hết các hệ thống SNARKs được xây dựng thường bao gồm hai phần sau:

• Chứng minh Oracle tương tác đa thức lý thuyết thông tin (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP): PIOP, như là trung tâm của hệ thống chứng minh, chuyển đổi các mối quan hệ tính toán đầu vào thành các phương trình đa thức có thể xác minh. Các giao thức PIOP khác nhau cho phép người chứng minh gửi từng bước một đa thức thông qua tương tác với người xác minh, giúp người xác minh có thể xác minh tính chính xác của phép tính chỉ bằng cách truy vấn một số lượng nhỏ các kết quả đánh giá đa thức. Các giao thức PIOP hiện có bao gồm: PLONK PIOP, Spartan PIOP và HyperPlonk PIOP, mỗi giao thức đều có cách xử lý các biểu thức đa thức khác nhau, từ đó ảnh hưởng đến hiệu suất và hiệu quả của toàn bộ hệ thống SNARK.

• Kế hoạch cam kết đa thức ( Polynomial Commitment Scheme, PCS ): Kế hoạch cam kết đa thức được sử dụng để chứng minh xem phương trình đa thức được tạo ra bởi PIOP có đúng hay không. PCS là một công cụ mật mã, thông qua đó, người chứng minh có thể cam kết một đa thức và sau đó xác minh kết quả đánh giá của đa thức đó, đồng thời ẩn giấu thông tin khác của đa thức. Các kế hoạch cam kết đa thức phổ biến bao gồm KZG, Bulletproofs, FRI ( Fast Reed-Solomon IOPP ) và Brakedown, v.v. Các PCS khác nhau có hiệu suất, độ an toàn và các trường hợp sử dụng khác nhau.

Dựa trên nhu cầu cụ thể, chọn PIOP và PCS khác nhau, và kết hợp với miền hữu hạn hoặc đường cong Elliptic phù hợp, có thể xây dựng hệ thống chứng minh với các thuộc tính khác nhau. Ví dụ:

• Halo2: Kết hợp giữa PLONK PIOP và Bulletproofs PCS, và dựa trên đường cong Pasta. Halo2 được thiết kế chú trọng vào khả năng mở rộng, cũng như loại bỏ thiết lập tin cậy trong giao thức ZCash.

• Plonky2: Sử dụng PLONK PIOP kết hợp với FRI PCS và dựa trên miền Goldilocks. Plonky2 được thiết kế để thực hiện đệ quy hiệu quả. Khi thiết kế các hệ thống này, PIOP và PCS được chọn phải phù hợp với miền hữu hạn hoặc đường cong ellip mà đang sử dụng, để đảm bảo tính chính xác, hiệu suất và độ an toàn của hệ thống. Sự lựa chọn của các tổ hợp này không chỉ ảnh hưởng đến kích thước chứng minh SNARK và hiệu quả xác minh, mà còn quyết định xem hệ thống có thể đạt được tính minh bạch mà không cần thiết lập đáng tin cậy hay không, và liệu có thể hỗ trợ các chức năng mở rộng như chứng minh đệ quy hoặc chứng minh tổng hợp.

Binius: HyperPlonk PIOP + Brakedown PCS + miền nhị phân. Cụ thể, Binius bao gồm năm công nghệ then chốt để đạt được hiệu suất và an ninh của nó. Đầu tiên, dựa trên miền nhị phân dạng tháp (towers of binary fields), sự tính toán này đã tạo thành nền tảng cho việc tính toán của nó, có khả năng thực hiện các phép toán đơn giản trong miền nhị phân. Thứ hai, Binius trong giao thức chứng minh Oracle tương tác của nó (PIOP), đã cải biên kiểm tra sản phẩm và hoán vị HyperPlonk, đảm bảo kiểm tra tính nhất quán an toàn và hiệu quả giữa các biến và sự hoán vị của chúng. Thứ ba, giao thức giới thiệu một chứng minh dịch chuyển đa tuyến mới, tối ưu hóa hiệu quả xác minh mối quan hệ đa tuyến trên miền nhỏ. Thứ tư, Binius đã áp dụng phiên bản cải tiến của chứng minh tìm kiếm Lasso, cung cấp sự linh hoạt và an ninh mạnh mẽ cho cơ chế tìm kiếm. Cuối cùng, giao thức sử dụng kế hoạch cam kết đa thức miền nhỏ (Small-Field PCS), cho phép nó thực hiện hệ thống chứng minh hiệu quả trên miền nhị phân và giảm thiểu chi phí thường liên quan đến miền lớn.

2.1 Tập hợp hữu hạn: Toán tử số học dựa trên các tháp của trường nhị phân

Trường nhị phân theo kiểu tháp là chìa khóa để thực hiện tính toán có thể xác minh nhanh chóng, chủ yếu nhờ vào hai khía cạnh: tính toán hiệu quả và tính toán hóa hiệu quả. Trường nhị phân về bản chất hỗ trợ các phép toán số học rất hiệu quả, khiến nó trở thành lựa chọn lý tưởng cho các ứng dụng mật mã nhạy cảm về hiệu suất. Ngoài ra, cấu trúc trường nhị phân hỗ trợ quy trình tính toán hóa đơn giản, tức là các phép toán thực hiện trên trường nhị phân có thể được biểu diễn dưới dạng đại số gọn gàng và dễ xác minh. Những đặc điểm này, cùng với khả năng khai thác triệt để đặc điểm phân cấp của nó thông qua cấu trúc tháp, khiến trường nhị phân đặc biệt phù hợp với các hệ thống chứng minh có thể mở rộng như Binius.

Trong đó, "canonical" chỉ cách biểu diễn duy nhất và trực tiếp của các phần tử trong miền nhị phân. Ví dụ, trong miền nhị phân cơ bản F2, bất kỳ chuỗi k bit nào cũng có thể được ánh xạ trực tiếp thành một phần tử miền nhị phân k bit. Điều này khác với miền số nguyên tố, miền số nguyên tố không thể cung cấp cách biểu diễn tiêu chuẩn này trong một số bit đã cho. Mặc dù miền số nguyên tố 32 bit có thể chứa trong 32 bit, nhưng không phải mọi chuỗi 32 bit đều có thể tương ứng duy nhất với một phần tử miền, trong khi miền nhị phân lại có sự thuận lợi trong ánh xạ một-một này. Trong miền số nguyên tố Fp, các phương pháp giảm phổ biến bao gồm giảm Barrett, giảm Montgomery, và các phương pháp giảm đặc biệt cho các miền hữu hạn cụ thể như Mersenne-31 hoặc Goldilocks-64. Trong miền nhị phân F2k, các phương pháp giảm thường được sử dụng bao gồm giảm đặc biệt ( như trong AES sử dụng ), giảm Montgomery ( như trong POLYVAL sử dụng ) và giảm đệ quy ( như Tower ). Bài báo "Khám Phá Không Gian Thiết Kế của ECC-Hardware Thực Hiện Trên Miền Số Nguyên Tố So Với Miền Nhị Phân" chỉ ra rằng miền nhị phân không cần phải đưa vào chuyển đổi trong các phép toán cộng và nhân, và phép toán bình phương trong miền nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản hóa (X + Y )2 = X2 + Y2.

Như hình 1 cho thấy, một chuỗi 128 bit: chuỗi này có thể được diễn giải theo nhiều cách trong bối cảnh miền nhị phân. Nó có thể được coi là một phần tử duy nhất trong miền nhị phân 128 bit, hoặc được phân tích thành hai phần tử miền tháp 64 bit, bốn phần tử miền tháp 32 bit, mười sáu phần tử miền tháp 8 bit, hoặc 128 phần tử miền F2. Tính linh hoạt trong biểu diễn này không yêu cầu bất kỳ chi phí tính toán nào, chỉ cần chuyển đổi kiểu của chuỗi bit (typecast), đây là một thuộc tính rất thú vị và hữu ích. Đồng thời, các phần tử miền nhỏ có thể được đóng gói thành các phần tử miền lớn hơn mà không cần chi phí tính toán bổ sung. Giao thức Binius đã tận dụng đặc điểm này để cải thiện hiệu quả tính toán. Ngoài ra, tài liệu "On Efficient Inversion in Tower Fields of Characteristic Two" khám phá độ phức tạp tính toán của phép nhân, phép bình phương và phép đảo trong miền tháp nhị phân n bit có thể phân tách thành miền con m bit (.

![Bitlayer Research：Phân tích nguyên lý Binius STARKs và suy nghĩ về tối ưu hóa])https://img-cdn.gateio.im/webp-social/moments-5775a629f494c4e01e2b74d864fa4100.webp(

) 2.2 PIOP: Phiên bản chỉnh sửa HyperPlonk Product và PermutationCheck------Thích hợp cho trường nhị phân

Thiết kế PIOP trong giao thức Binius đã tham khảo HyperPlonk, sử dụng một loạt các cơ chế kiểm tra cốt lõi, nhằm xác thực tính chính xác của đa thức và tập hợp đa biến. Những kiểm tra cốt lõi này bao gồm:

1. GateCheck: Xác minh chứng nhận bí mật ω và đầu vào công khai x có thỏa mãn quan hệ toán tử mạch C###x, ω(=0, để đảm bảo mạch hoạt động đúng.

2. PermutationCheck: Xác minh xem kết quả đánh giá của hai đa thức nhiều biến f và g trên lập phương siêu Boolean có phải là quan hệ hoán vị hay không f)x( = f)π(x(), để đảm bảo tính nhất quán của sự sắp xếp giữa các biến đa thức.

3. LookupCheck: Xác minh xem giá trị của đa thức có nằm trong bảng tra cứu đã cho hay không, tức là f)Bµ( ⊆ T)Bµ(, đảm bảo rằng một số giá trị nằm trong phạm vi chỉ định.

4. MultisetCheck: Kiểm tra xem hai tập hợp đa biến có bằng nhau hay không, tức là {)x1,i,x2,(}i∈H={)y1,i,y2,(}i∈H, đảm bảo tính nhất quán giữa nhiều tập hợp.

5. ProductCheck: Kiểm tra giá trị của đa thức hữu tỷ trên hypercube Boolean có bằng với một giá trị được tuyên bố nào đó ∏x∈Hµ f)x( = s, để đảm bảo tính chính xác của tích đa thức.

6. ZeroCheck: Xác minh xem một đa biến đa thức tại bất kỳ điểm nào trên siêu lập phương Boolean có phải là bằng không hay không ∏x∈Hµ f)x( = 0, ∀x ∈ Bµ, để đảm bảo phân bố của các điểm không của đa thức.

7. SumCheck: Kiểm tra xem tổng của đa thức nhiều biến có bằng giá trị đã tuyên bố hay không ∑x∈Hµ f)x( = s. Bằng cách chuyển đổi vấn đề đánh giá đa thức nhiều biến thành đánh giá đa thức một biến, giảm độ phức tạp tính toán của bên xác minh. Ngoài ra, SumCheck còn cho phép xử lý hàng loạt, thông qua việc giới thiệu số ngẫu nhiên, xây dựng tổ hợp tuyến tính để thực hiện việc kiểm tra hàng loạt nhiều trường hợp tổng.

8. BatchCheck: Dựa trên SumCheck, xác minh tính chính xác của nhiều giá trị đa thức nhiều biến, nhằm nâng cao hiệu quả của giao thức.

Mặc dù Binius và HyperPlonk có nhiều điểm tương đồng trong thiết kế giao thức, nhưng Binius đã cải tiến ở 3 khía cạnh sau:

• Tối ưu hóa ProductCheck: Trong HyperPlonk, ProductCheck yêu cầu mẫu số U không được bằng 0 ở mọi điểm trong siêu lập phương, và tích phải bằng một giá trị cụ thể; Binius đã đơn giản hóa quy trình kiểm tra này bằng cách đặc biệt hóa giá trị đó thành 1, từ đó giảm độ phức tạp tính toán.

• Xử lý vấn đề chia cho 0: HyperPlonk không thể xử lý đầy đủ tình huống chia cho 0, dẫn đến không thể khẳng định vấn đề khác không của U trên siêu lập phương; Binius đã xử lý đúng vấn đề này, ngay cả khi mẫu số bằng 0, ProductCheck của Binius vẫn có thể tiếp tục xử lý, cho phép mở rộng đến giá trị tích bất kỳ.

• Kiểm tra hoán vị giữa các cột: HyperPlonk không có tính năng này; Binius hỗ trợ kiểm tra hoán vị giữa nhiều cột, điều này cho phép Binius xử lý các tình huống sắp xếp đa thức phức tạp hơn.

Do đó, Binius đã cải thiện cơ chế PIOPSumCheck hiện có, nâng cao tính linh hoạt và hiệu quả của giao thức, đặc biệt là khi xử lý xác minh đa biến đa thức phức tạp hơn, cung cấp hỗ trợ chức năng mạnh mẽ hơn. Những cải tiến này không chỉ giải quyết các hạn chế trong HyperPlonk mà còn đặt nền tảng cho các hệ thống chứng minh dựa trên trường nhị phân trong tương lai.

) 2.3 PIOP: lập luận dịch tuyến tính mới------áp dụng cho hypercube boolean

Trong giao thức Binius, việc xây dựng và xử lý đa thức ảo là một trong những công nghệ chính, có khả năng tạo ra và thao tác hiệu quả các đa thức được phát sinh từ tay cầm đầu vào hoặc các đa thức ảo khác. Dưới đây là hai phương pháp then chốt:

• Đóng gói: Phương pháp này tối ưu hóa hoạt động bằng cách đóng gói các phần tử nhỏ hơn ở các vị trí liền kề trong thứ tự từ điển thành các phần tử lớn hơn. Toán tử Pack nhắm đến các khối có kích thước 2κ và kết hợp chúng thành các chiều cao hơn.