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

1 Giới thiệu

Một lý do chính khiến STARKs kém hiệu quả là hầu hết các giá trị trong chương trình thực tế đều nhỏ, nhưng để đảm bảo tính an toàn của bằng chứng dựa trên cây Merkle, khi sử dụng mã Reed-Solomon để mở rộng dữ liệu, nhiều giá trị dư thừa bổ sung sẽ chiếm toàn bộ miền, ngay cả khi giá trị ban đầu rất nhỏ. Để giải quyết vấn đề này, việc giảm kích thước miền trở thành một chiến lược quan trọng.

Độ rộng mã hóa của STARKs thế hệ đầu tiên là 252bit, độ rộng mã hóa của STARKs thế hệ thứ hai là 64bit, độ rộng mã hóa của STARKs thế hệ thứ ba là 32bit, nhưng độ rộng mã hóa 32bit vẫn cò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ẽ và hiệu quả mà 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ề trường hữu hạn, nghiên cứu về trường nhị phân có thể truy ngược lại từ những năm 80 của thế kỷ trước. Hiện nay, trường nhị phân đã được ứng dụng rộng rãi trong mật mã học, 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ã Reed-Solomon dựa trên F28;

• Giao thức FRI gốc và zk-STARK, cũng như hàm băm Grøstl vào vòng chung kết SHA-3, hàm băm này dựa trên miền F28, là một thuật toán băm rất phù hợp cho việc đệ 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 tính bảo mật. 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 tính bảo mật và khả năng sử dụng thực tế. Hầu hết các đa thức liên quan trong 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 quả cao trong miền nhỏ. Tuy nhiên, việc 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 tính bảo mật 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 cây Merkle 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 sáng tạo để xử lý hai vấn đề này một cách riêng biệt, và đạt được điều đó bằng cách biểu diễn 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) thay thế cho đa thức đơn biến, thông qua các giá trị của nó trên "hình lập phương siêu" (hypercubes) để biểu diễn toàn bộ quỹ đạo tính toán; thứ hai, do chiều dài của mỗi chiều của hình lập phương siêu đều là 2, nên không thể thực hiện mở rộng Reed-Solomon theo cách tiêu chuẩn như STARKs, nhưng có thể coi hình lập phương siêu là hình vuông (square), và thực hiện mở rộng Reed-Solomon dựa trên hình vuông đó. Phương pháp này đảm bảo tính an toàn trong khi đồng thời nâng cao 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 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 là cốt lõi của hệ thống chứng minh, chuyển đổi 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 dần dần các đa thức thông qua sự tương tác với người xác minh, cho phép người xác minh xác nhận xem tính toán có đúng hay không chỉ bằng cách truy vấn một lượng nhỏ 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 có cách xử lý 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.

• Phương án cam kết đa thức (Polynomial Commitment Scheme, PCS): Phương án 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ó hợp lệ 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 đi các thông tin khác về đa thức. Một số phương án cam kết đa thức phổ biến bao gồm KZG, Bulletproofs, FRI (Fast Reed-Solomon IOPP) và Brakedown. Các PCS khác nhau có hiệu suất, độ an toàn và ngữ cảnh áp dụng khác nhau.

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

• Halo2: Được kết hợp từ PLONK PIOP và Bulletproofs PCS, và dựa trên đường cong Pasta. Halo2 được thiết kế với sự chú trọng đến khả năng mở rộng, cũng như loại bỏ việc 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 việc đệ quy hiệu quả. Khi thiết kế những hệ thống này, PIOP và PCS được chọn phải tương thích với miền hữu hạn hoặc đường cong elliptic được 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 những kết hợp này không chỉ ảnh hưởng đến kích thước chứng minh SNARK và hiệu suất 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, và có thể hỗ trợ các tính năng mở rộng như chứng minh đệ quy hoặc chứng minh tổng hợp hay không.

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 toàn của nó. Đầu tiên, cấu trúc toán học dựa trên tháp miền nhị phân (towers of binary fields) tạo thành nền tảng cho tính toán của nó, cho phép thực hiện các phép toán đơn giản trong miền nhị phân. Thứ hai, Binius đã điều chỉnh kiểm tra tích và hoán đổi HyperPlonk trong giao thức chứng minh Oracle tương tác của nó (PIOP), đả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 đổi 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 các mối quan hệ đa tuyến trên miền nhỏ. Thứ tư, Binius sử dụng chứng minh tìm kiếm Lasso phiên bản cải tiến, cung cấp sự linh hoạt và độ an toàn mạnh mẽ cho cơ chế tìm kiếm. Cuối cùng, giao thức sử dụng phương án cam kết đa thức miền nhỏ (Small-Field PCS), cho phép nó thiết lập 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 Miền hữu hạn: Toán tử dựa trên các tháp của trường nhị phân

Miền nhị phân 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 do hai yếu tố: tính toán hiệu quả và phép toán hiệu quả. Miền nhị phân về bản chất hỗ trợ các phép toán số học hiệu quả cao, làm cho 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ới yêu cầu về hiệu suất. Ngoài ra, cấu trúc miền nhị phân hỗ trợ quy trình số học đơn giản hóa, tức là các phép toán thực hiện trên miền 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 tận dụng đầy đủ các đặc tính phân cấp của nó thông qua cấu trúc tháp, khiến miền 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" đề cập đến cách biểu diễn duy nhất và trực tiếp của các phần tử trong trường nhị phân. Ví dụ, trong trường 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 tới một phần tử trường nhị phân k bit. Điều này khác với trường số nguyên tố, nơi mà không thể cung cấp được cách biểu diễn chuẩn như vậy trong một số bit nhất định. Mặc dù trường số nguyên tố 32 bit có thể bao gồm trong 32 bit, nhưng không phải tất cả các chuỗi 32 bit đều có thể tương ứng một cách duy nhất với một phần tử của trường, trong khi trường nhị phân lại có sự tiện lợi của ánh xạ một-một này. Trong trường số nguyên tố Fp, các phương pháp giảm thiểu phổ biến bao gồm giảm thiểu Barrett, giảm thiểu Montgomery, và các phương pháp giảm thiểu đặc biệt cho các trường hữu hạn cụ thể như Mersenne-31 hoặc Goldilocks-64. Trong trường nhị phân F2k, các phương pháp giảm thiểu thường được sử dụng bao gồm giảm thiểu đặc biệt (như được sử dụng trong AES), giảm thiểu Montgomery (như được sử dụng trong POLYVAL) và giảm thiểu đệ quy (như Tower). Bài báo "Khám Phá Không Gian Thiết Kế của Các Cài Đặt Phần Cứng ECC Trường Số Nguyên Tố So Với Trường Nhị Phân" chỉ ra rằng trường nhị phân không cần phải đưa vào sự chuyển vị trong các phép toán cộng và nhân, và phép toán bình phương trong trường nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản (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 giải thích theo nhiều cách trong ngữ cảnh của miền nhị phân. Nó có thể được coi là một phần tử độc 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 một trăm hai mươi tám phần tử miền F2. Tính linh hoạt của biểu diễn này không cần bất kỳ chi phí tính toán nào, chỉ là một chuyển đổi kiểu (typecast) của chuỗi bit, 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 gói lại thành các phần tử miền lớn hơn mà không cần thêm chi phí tính toán. Giao thức Binius đã tận dụng đặc điểm này để cải thiện hiệu quả tính toán. Hơn nữa, bài báo "On Efficient Inversion in Tower Fields of Characteristic Two" đã khám phá độ phức tạp tính toán của các phép nhân, bình phương và tìm nghịch đảo trong miền nhị phân tháp n bit (có thể phân rã thành miền con m bit).

2.2 PIOP: Phiên bản cải biên HyperPlonk Product và PermutationCheck------Áp dụng 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ơ chế kiểm tra cốt lõi để xác minh độ chính xác của đa thức và tập hợp nhiều biến. Những kiểm tra cốt lõi này bao gồm:

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

2. PermutationCheck: Xác thực xem kết quả đánh giá của hai đa thức nhiều biến f và g trên siêu khối Boolean có phải là quan hệ hoán vị hay không f(x) = f(π(x)), nhằm đả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 xem giá trị của đa thức có lý trong lập phương siêu Boolean có bằng một giá trị đã được tuyên bố nào đó ∏x∈Hµ f(x) = s hay không, để đảm bảo tính chính xác của tích đa thức.

6. ZeroCheck: Xác minh một đa biến đa thức tại bất kỳ điểm nào trên siêu khối Boolean có phải là không ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, để đảm bảo sự 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 với giá trị đã khai báo ∑x∈Hµ f(x) = s hay không. Bằng cách biế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ý theo lô, 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 tổng nhiều trường hợp.

8. BatchCheck: Dựa trên SumCheck, xác minh tính chính xác của nhiều giá trị đa biến đa thức để cải thiện 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 điểm sau:

• Tối ưu hóa ProductCheck: Trong HyperPlonk, ProductCheck yêu cầu mẫu số U không được bằng 0 trên 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 quá 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 không: HyperPlonk không xử lý tốt trường hợp chia cho không, dẫn đến không thể khẳng định vấn đề không bằng không của U trên siêu khối; Binius đã xử lý đúng vấn đề này, ngay cả khi mẫu số bằng không, ProductCheck của Binius vẫn có thể tiếp tục xử lý, cho phép mở rộng đến bất kỳ giá trị tích nào.

• 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 tiế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 trong việc xử lý các 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 những 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 miền nhị phân trong tương lai.

2.3 PIOP：tham số dịch nhiều dòng 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ệ then chốt, 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 quan trọng:

• Đóng gói：Phương pháp này thông qua việc đánh đống các phần tử nhỏ hơn ở các vị trí liền kề trong thứ tự từ điển.