Xác minh hình thức tiên tiến cho bằng chứng không kiến thức: Phân tích sâu hai lỗ hổng ZK
Tuyển chọn TechFlowTuyển chọn TechFlow
Xác minh hình thức tiên tiến cho bằng chứng không kiến thức: Phân tích sâu hai lỗ hổng ZK
Trong bài viết này, chúng ta sẽ tập trung vào góc nhìn phát hiện lỗ hổng, phân tích các lỗ hổng cụ thể được tìm thấy trong quá trình kiểm toán và xác minh, cũng như những kinh nghiệm và bài học rút ra từ đó.
Chuyên sâu báo cáo Web3Tác giả: CertiK
Trong các bài viết trước, chúng tôi đã thảo luận về xác minh hình thức tiên tiến đối với bằng chứng kiến thức không (ZKP): cách xác minh một lệnh zk. Bằng việc xác minh hình thức từng lệnh zkWasm, chúng tôi có thể hoàn toàn đảm bảo tính an toàn kỹ thuật và tính đúng đắn của toàn bộ mạch zkWasm. Trong bài viết này, chúng tôi sẽ tiếp cận từ góc độ phát hiện lỗ hổng, phân tích những lỗ hổng cụ thể được tìm thấy trong quá trình kiểm toán và xác minh, cũng như rút ra bài học kinh nghiệm từ đó. Để tìm hiểu thêm về xác minh hình thức tiên tiến đối với blockchain bằng chứng kiến thức không (ZKP), vui lòng tham khảo bài viết “Xác minh hình thức tiên tiến đối với blockchain ZKP”.
Trước khi đi vào thảo luận về các lỗ hổng ZK, hãy cùng tìm hiểu cách CertiK thực hiện xác minh hình thức (FV) đối với hệ thống ZK. Đối với các hệ thống phức tạp như máy ảo ZK (zkVM), bước đầu tiên của xác minh hình thức là xác định rõ nội dung cần xác minh và các thuộc tính liên quan. Điều này đòi hỏi phải xem xét toàn diện thiết kế hệ thống ZK, mã nguồn triển khai và cấu hình kiểm thử. Quá trình này phần nào trùng lặp với kiểm toán thông thường, nhưng điểm khác biệt nằm ở chỗ sau khi xem xét, cần xác lập mục tiêu và đặc tính để xác minh. Tại CertiK, chúng tôi gọi đây là kiểm toán hướng tới xác minh. Công việc kiểm toán và xác minh thường diễn ra đồng thời. Với zkWasm, chúng tôi đã thực hiện cả kiểm toán lẫn xác minh hình thức.
Lỗ hổng ZK là gì?
Đặc điểm cốt lõi của hệ thống bằng chứng kiến thức không (zero-knowledge proof - ZKP) là cho phép truyền tải một bằng chứng mã hóa ngắn gọn về một phép tính được thực hiện ngoại tuyến hoặc riêng tư (ví dụ như giao dịch blockchain) đến bộ kiểm tra ZKP, nơi nó sẽ được kiểm tra và xác nhận để đảm bảo rằng phép tính đó thực sự đã xảy ra như đã tuyên bố. Theo nghĩa này, một lỗ hổng ZK cho phép tin tặc gửi một bằng chứng ZK giả mạo nhằm chứng minh một giao dịch sai lệch và khiến bộ kiểm tra ZK chấp nhận nó.
Đối với bộ tạo bằng chứng của zkVM, quy trình tạo bằng chứng ZK bao gồm chạy chương trình, ghi lại từng bước thực thi và chuyển đổi dữ liệu bản ghi thực thi thành một tập hợp bảng số (quá trình này gọi là "số học hóa"). Các con số trong các bảng này phải thỏa mãn một tập hợp ràng buộc (tức là "mạch"), bao gồm các phương trình liên kết giữa các ô bảng cụ thể, các hằng số cố định, các ràng buộc tra cứu cơ sở dữ liệu giữa các bảng, và các phương trình đa thức cần được thỏa mãn giữa từng cặp hàng liền kề trong bảng (còn gọi là "cổng"). Việc xác minh trên chuỗi do đó có thể khẳng định rằng thực sự tồn tại một bảng thỏa mãn tất cả các ràng buộc mà không cần nhìn thấy các con số cụ thể trong bảng đó.
Bảng số học hóa zkWasm
Tính chính xác của mỗi ràng buộc đều cực kỳ quan trọng. Một lỗi nhỏ trong bất kỳ ràng buộc nào, dù là yếu hoặc thiếu, đều có thể cho phép tin tặc gửi một bằng chứng gây hiểu lầm — những bảng biểu dường như đại diện cho một lần chạy hợp lệ của hợp đồng thông minh nhưng thực tế thì không phải vậy. So với máy ảo (VM) truyền thống, tính chất mờ ám của giao dịch zkVM làm trầm trọng thêm các lỗ hổng này. Trên các chuỗi không dùng ZK, chi tiết tính toán của giao dịch được công khai ghi lại trên khối; còn zkVM thì không lưu trữ chi tiết này trên chuỗi. Sự thiếu minh bạch khiến rất khó xác định được chi tiết tấn công, thậm chí khó xác định được liệu một cuộc tấn công đã xảy ra hay chưa.
Các mạch ZK điều khiển quy tắc thực thi lệnh zkVM cực kỳ phức tạp. Với zkWasm, việc triển khai mạch ZK liên quan đến hơn 6.000 dòng mã Rust và hàng trăm ràng buộc. Mức độ phức tạp này thường hàm ý rằng có thể tồn tại nhiều lỗ hổng đang chờ được phát hiện.
Kiến trúc mạch zkWasm
Thực tế đúng như vậy: qua kiểm toán và xác minh hình thức đối với zkWasm, chúng tôi đã phát hiện nhiều lỗ hổng như vậy. Dưới đây, chúng tôi sẽ thảo luận hai ví dụ tiêu biểu và phân tích sự khác biệt giữa chúng.
Lỗ hổng mã nguồn: Tấn công tiêm dữ liệu Load8
Lỗ hổng đầu tiên liên quan đến lệnh Load8 của zkWasm. Trong zkWasm, việc đọc vùng nhớ heap được thực hiện thông qua một nhóm lệnh LoadN, trong đó N là kích thước dữ liệu cần tải. Ví dụ, lệnh Load64 nên đọc dữ liệu 64 bit từ địa chỉ bộ nhớ zkWasm. Lệnh Load8 nên đọc dữ liệu 8 bit (tức là một byte) từ bộ nhớ và điền thêm số 0 phía trước để tạo giá trị 64 bit. Bên trong zkWasm, bộ nhớ được biểu diễn dưới dạng mảng các từ 64 bit, do đó cần "trích xuất" một phần của mảng bộ nhớ. Để làm điều này, sử dụng bốn biến trung gian (u16_cells), khi kết hợp lại sẽ tạo thành giá trị tải đầy đủ 64 bit.
Ràng buộc định nghĩa các lệnh LoadN như sau:
Ràng buộc này được chia thành ba trường hợp: Load32, Load16 và Load8. Load64 không có ràng buộc nào vì đơn vị bộ nhớ đúng bằng 64 bit. Trường hợp Load32, mã đảm bảo rằng 4 byte cao (32 bit) trong đơn vị bộ nhớ phải bằng 0.
Trường hợp Load16, 6 byte cao (48 bit) trong đơn vị bộ nhớ phải bằng 0.
Trường hợp Load8, đáng lẽ phải yêu cầu 7 byte cao (56 bit) trong đơn vị bộ nhớ bằng 0. Đáng tiếc là trong mã nguồn lại không như vậy.
Như bạn thấy, chỉ có các bit từ 9 đến 16 cao hơn bị giới hạn bằng 0. 48 bit cao khác có thể mang bất kỳ giá trị nào, nhưng vẫn giả mạo được là "được đọc từ bộ nhớ".
Bằng cách khai thác lỗ hổng này, tin tặc có thể sửa đổi bằng chứng ZK của một chuỗi thực thi hợp lệ sao cho lệnh Load8 tải các byte bất ngờ này, dẫn đến hỏng dữ liệu. Hơn nữa, bằng cách sắp xếp cẩn thận mã và dữ liệu xung quanh, có thể kích hoạt các lần thực thi và chuyển tiền giả mạo, từ đó đánh cắp dữ liệu và tài sản. Giao dịch giả mạo này có thể vượt qua kiểm tra của bộ kiểm tra zkWasm và bị blockchain coi nhầm là giao dịch thật.
Việc sửa lỗ hổng này thực ra khá đơn giản.
Lỗ hổng này đại diện cho một lớp các lỗ hổng ZK được gọi là "lỗ hổng mã nguồn", bởi vì chúng bắt nguồn từ việc viết mã và có thể dễ dàng sửa bằng những thay đổi cục bộ nhỏ trong mã. Như bạn có thể đồng ý, những lỗ hổng này cũng tương đối dễ phát hiện bằng mắt thường.
Lỗ hổng thiết kế: Tấn công trả về giả mạo
Hãy xem xét một lỗ hổng khác, lần này liên quan đến việc gọi và trả về trong zkWasm. Gọi và trả về là các lệnh VM cơ bản, cho phép một ngữ cảnh đang chạy (ví dụ như một hàm) gọi một ngữ cảnh khác và sau khi ngữ cảnh được gọi hoàn tất thực thi, phục hồi việc thực thi của ngữ cảnh gọi. Mỗi lần gọi đều dự kiến sẽ có một lần trả về tương ứng sau đó. Dữ liệu động được theo dõi bởi zkWasm trong suốt vòng đời gọi và trả về được gọi là "khung gọi (call frame)". Vì zkWasm thực thi tuần tự các lệnh, tất cả các khung gọi có thể được sắp xếp theo thứ tự thời gian xảy ra trong quá trình thực thi. Dưới đây là một ví dụ về mã gọi/trả về chạy trên zkWasm.
Người dùng có thể gọi hàm buy_token() để mua token (có thể bằng cách thanh toán hoặc chuyển một thứ có giá trị khác). Một trong những bước cốt lõi của nó là gọi hàm add_token() để thực sự tăng số dư tài khoản token lên 1. Do bộ tạo bằng chứng ZK không hỗ trợ cấu trúc dữ liệu khung gọi, nên cần sử dụng bảng thực thi (E-Table) và bảng nhảy (J-Table) để ghi lại và theo dõi toàn bộ lịch sử các khung gọi.
Hình trên minh họa quá trình buy_token() gọi add_token() và sau đó trả về từ add_token() về buy_token(). Có thể thấy số dư tài khoản token tăng lên 1. Trong bảng thực thi, mỗi bước thực thi chiếm một hàng, bao gồm số hiệu khung gọi hiện tại, tên hàm ngữ cảnh hiện tại (chỉ dùng để minh họa), số hiệu lệnh hiện tại bên trong hàm đó, và lệnh hiện tại được lưu trong bảng (chỉ dùng để minh họa). Trong bảng nhảy, mỗi khung gọi chiếm một hàng, chứa số hiệu khung gọi của người gọi, tên ngữ cảnh hàm của người gọi (chỉ dùng để minh họa), vị trí lệnh tiếp theo của khung gọi (để khung đó có thể trở về). Cả hai bảng đều có cột jops, dùng để theo dõi xem lệnh hiện tại có phải là gọi/trả về (trong bảng thực thi) và tổng số lệnh gọi/trả về xảy ra trên khung đó (trong bảng nhảy).
Như mong đợi, mỗi lần gọi nên có đúng một lần trả về, và mỗi khung chỉ nên có đúng một lần gọi và một lần trả về. Như hình trên, giá trị jops của khung 1 trong bảng nhảy là 2, khớp với hai hàng trong bảng thực thi (hàng 1 và 3) nơi jops bằng 1. Hiện tại mọi thứ dường như ổn.
Tuy nhiên thực tế tồn tại một vấn đề: mặc dù một lần gọi và một lần trả về sẽ làm cho jops của khung bằng 2, nhưng hai lần gọi hoặc hai lần trả về cũng sẽ làm jops bằng 2. Việc mỗi khung có hai lần gọi hoặc hai lần trả về nghe có vẻ vô lý, nhưng hãy nhớ rằng chính điều này là điều mà tin tặc muốn phá vỡ kỳ vọng để thực hiện.
Bạn có thể đang cảm thấy phấn khích, nhưng liệu chúng ta đã thực sự tìm ra vấn đề chưa?
Hóa ra, hai lần gọi không phải là vấn đề, bởi vì các ràng buộc trên bảng thực thi và bảng gọi ngăn không cho hai lần gọi được mã hóa vào cùng một hàng của khung, vì mỗi lần gọi sẽ tạo ra một số hiệu khung mới, bằng số hiệu khung hiện tại cộng thêm 1.
Tuy nhiên, trường hợp hai lần trả về thì không may mắn như vậy: vì việc trả về không tạo ra khung mới, tin tặc thực sự có thể lấy bảng thực thi và bảng gọi của một chuỗi thực thi hợp lệ và tiêm vào các lần trả về giả mạo (và khung tương ứng). Ví dụ, ví dụ trước về việc buy_token() gọi add_token() trong bảng thực thi và bảng gọi có thể bị tin tặc sửa đổi thành như sau:
Tin tặc chèn hai lần trả về giả mạo giữa lần gọi và trả về ban đầu trong bảng thực thi, đồng thời thêm một hàng khung giả mạo mới vào bảng nhảy (các bước thực thi sau lần trả về ban đầu trong bảng thực thi cần tăng số hiệu thêm 4). Vì mỗi hàng trong bảng nhảy đều có jops bằng 2, nên ràng buộc được thỏa mãn, và bộ kiểm tra zkWasm sẽ chấp nhận "bằng chứng" của chuỗi thực thi giả mạo này. Như có thể thấy trong hình, số dư tài khoản token được tăng 3 lần thay vì 1 lần. Do đó, tin tặc có thể nhận được 3 token chỉ với giá 1 token.
Có nhiều cách để giải quyết vấn đề này. Một cách rõ ràng là theo dõi riêng biệt số lần gọi và trả về, và đảm bảo mỗi khung có đúng một lần gọi và một lần trả về.
Bạn có thể đã nhận thấy rằng đến nay chúng tôi chưa hề hiển thị một dòng mã nào của lỗ hổng này. Lý do chủ yếu là vì không có dòng mã nào sai cả — mã triển khai hoàn toàn phù hợp với thiết kế bảng và ràng buộc. Vấn đề nằm ở chính thiết kế, và cách sửa chữa cũng thuộc về thiết kế.
Bạn có thể nghĩ rằng lỗ hổng này hẳn phải rõ ràng, nhưng thực tế không phải vậy. Bởi vì tồn tại một khoảng trống giữa "hai lần gọi hoặc hai lần trả về cũng làm jops bằng 2" và "thực tế hai lần trả về là khả thi". Điều sau đòi hỏi phải phân tích chi tiết, toàn diện tất cả các ràng buộc liên quan trong bảng thực thi và bảng nhảy, điều này rất khó thực hiện bằng suy luận phi hình thức đầy đủ.
So sánh hai lỗ hổng
Cả "lỗ hổng tiêm dữ liệu Load8" và "lỗ hổng trả về giả mạo" đều có thể cho phép tin tặc thao túng bằng chứng ZK, tạo ra giao dịch giả mạo, đánh lừa bộ kiểm tra bằng chứng và thực hiện đánh cắp hoặc chiếm đoạt. Nhưng bản chất và cách phát hiện của chúng lại hoàn toàn khác nhau.
"Lỗ hổng tiêm dữ liệu Load8" được phát hiện trong quá trình kiểm toán zkWasm. Đây không phải là việc dễ dàng, vì chúng tôi phải xem xét hơn 6.000 dòng mã Rust và hàng trăm ràng buộc cho hàng trăm lệnh zkWasm. Tuy vậy, lỗ hổng này vẫn tương đối dễ phát hiện và xác nhận. Vì lỗ hổng này đã được sửa trước khi bắt đầu xác minh hình thức, nên nó không xuất hiện trong quá trình xác minh. Nếu không phát hiện được trong kiểm toán, chúng tôi dự kiến sẽ phát hiện nó trong quá trình xác minh lệnh Load8.
"Lỗ hổng trả về giả mạo" được phát hiện trong quá trình xác minh hình thức sau kiểm toán. Một phần lý do chúng tôi không phát hiện ra nó trong kiểm toán là vì trong zkWasm có một cơ chế rất giống jops gọi là "mops", theo dõi các lệnh truy cập bộ nhớ tương ứng với dữ liệu lịch sử của mỗi đơn vị bộ nhớ trong quá trình chạy zkWasm. Ràng buộc đếm mops thực sự đúng, vì nó chỉ theo dõi một loại lệnh bộ nhớ duy nhất, tức là ghi bộ nhớ; và dữ liệu lịch sử của mỗi đơn vị bộ nhớ là bất biến và chỉ được ghi đúng một lần (mops = 1). Nhưng ngay cả khi chú ý đến lỗ hổng tiềm năng này trong kiểm toán, nếu không thực hiện suy luận hình thức nghiêm ngặt đối với tất cả các ràng buộc liên quan, chúng tôi vẫn không thể dễ dàng xác nhận hay loại trừ mọi khả năng, vì thực tế không có dòng mã nào sai cả.
Tóm lại, hai lỗ hổng này thuộc về hai loại khác nhau: "lỗ hổng mã nguồn" và "lỗ hổng thiết kế". Lỗ hổng mã nguồn tương đối rõ ràng, dễ phát hiện hơn (do có mã sai), và dễ suy luận, xác nhận hơn; lỗ hổng thiết kế có thể rất ẩn sâu, khó phát hiện hơn (không có mã "sai"), và khó suy luận, xác nhận hơn.
Thực hành tốt nhất để phát hiện lỗ hổng ZK
Dựa trên kinh nghiệm kiểm toán và xác minh hình thức zkVM cũng như các chuỗi ZK và không dùng ZK khác, dưới đây là một số khuyến nghị về cách tốt nhất để bảo vệ hệ thống ZK.
Kiểm tra cả mã nguồn lẫn thiết kế
Như đã nói, cả mã nguồn và thiết kế ZK đều có thể chứa lỗ hổng. Cả hai loại lỗ hổng này đều có thể làm tổn hại hệ thống ZK, do đó phải được loại bỏ trước khi hệ thống đi vào vận hành. So với hệ thống không dùng ZK, một vấn đề với hệ thống ZK là mọi cuộc tấn công đều khó phơi bày và phân tích hơn, vì chi tiết tính toán không được công khai hay lưu trữ trên chuỗi. Do đó, người ta có thể biết đã xảy ra tấn công nhưng không thể biết rõ về mặt kỹ thuật chuyện gì đã xảy ra. Điều này khiến chi phí của bất kỳ lỗ hổng ZK nào đều rất cao. Do đó, giá trị của việc đảm bảo an toàn hệ thống ZK ngay từ đầu cũng rất lớn.
Thực hiện kiểm toán lẫn xác minh hình thức
Hai lỗ hổng được trình bày ở đây lần lượt được phát hiện qua kiểm toán và xác minh hình thức. Có người cho rằng nếu đã dùng xác minh hình thức thì không cần kiểm toán nữa, vì mọi lỗ hổng đều sẽ bị phát hiện. Thực tế, chúng tôi khuyên nên thực hiện cả hai. Như đã giải thích ở đầu bài viết, một công việc xác minh hình thức chất lượng cao luôn bắt đầu bằng việc rà soát kỹ lưỡng, kiểm tra và suy luận phi hình thức đối với mã và thiết kế; và công việc này bản thân nó đã trùng lặp với kiểm toán. Ngoài ra, việc phát hiện và loại bỏ các lỗ hổng đơn giản hơn trong quá trình kiểm toán sẽ giúp cho việc xác minh hình thức trở nên đơn giản và hiệu quả hơn.
Nếu muốn vừa kiểm toán vừa xác minh hình thức một hệ thống ZK, thời điểm tốt nhất là thực hiện đồng thời hai công việc này, để kiểm toán viên và kỹ sư xác minh hình thức có thể hợp tác hiệu quả (có thể phát hiện thêm nhiều lỗ hổng hơn, vì đối tượng và mục tiêu xác minh cần đầu vào kiểm toán chất lượng cao).
Nếu dự án ZK của bạn đã từng được kiểm toán (tốt) hoặc nhiều lần kiểm toán (rất tốt), chúng tôi vẫn khuyên nên thực hiện xác minh hình thức mạch dựa trên kết quả kiểm toán trước đó. Kinh nghiệm kiểm toán và xác minh hình thức của chúng tôi đối với zkVM cũng như các dự án ZK và không dùng ZK khác liên tục cho thấy rằng xác minh thường phát hiện được những lỗ hổng bị bỏ sót và khó phát hiện trong kiểm toán. Do đặc tính của ZKP, mặc dù hệ thống ZK nên cung cấp tính an toàn và mở rộng tốt hơn cho blockchain so với giải pháp không dùng ZK, nhưng mức độ quan trọng của tính an toàn và đúng đắn của chính nó lại cao hơn rất nhiều so với hệ thống truyền thống không dùng ZK. Do đó, giá trị của việc xác minh hình thức chất lượng cao đối với hệ thống ZK cũng cao hơn rất nhiều so với hệ thống không dùng ZK.
Đảm bảo an toàn cho cả mạch lẫn hợp đồng thông minh
Ứng dụng ZK thường bao gồm hai phần: mạch và hợp đồng thông minh. Với ứng dụng dựa trên zkVM, có mạch zkVM chung và ứng dụng hợp đồng thông minh. Với ứng dụng không dựa trên zkVM, có mạch ZK chuyên biệt cho ứng dụng và hợp đồng thông minh tương ứng được triển khai trên chuỗi L1 hoặc đầu kia của cầu nối. Dựa trên zkVM Không dựa trên zkVM
Công việc kiểm toán và xác minh hình thức của chúng tôi đối với zkWasm chỉ tập trung vào mạch zkWasm. Từ góc độ an toàn tổng thể của ứng dụng ZK, việc kiểm toán và xác minh hình thức đối với hợp đồng thông minh của nó cũng rất quan trọng. Dù sao đi nữa, sau khi đã bỏ rất nhiều công sức để đảm bảo an toàn cho mạch, nếu chủ quan với hợp đồng thông minh mà dẫn đến ứng dụng cuối cùng bị tổn hại thì thật đáng tiếc.
Có hai loại hợp đồng thông minh đáng được chú ý đặc biệt. Thứ nhất là các hợp đồng thông minh trực tiếp xử lý bằng chứng ZK. Mặc dù quy mô của chúng có thể không lớn, nhưng rủi ro lại rất cao. Thứ hai là các hợp đồng thông minh cỡ trung đến lớn chạy trên zkVM. Chúng ta biết rằng đôi khi chúng rất phức tạp, và những hợp đồng có giá trị nhất nên được kiểm toán và xác minh, đặc biệt vì người ta không thể thấy chi tiết thực thi của chúng trên chuỗi. May mắn thay, sau nhiều năm phát triển, xác minh hình thức hợp đồng thông minh hiện đã khả dụng trong thực tiễn và sẵn sàng áp dụng cho các mục tiêu giá trị cao phù hợp.
Hãy tóm tắt ảnh hưởng của xác minh hình thức (FV) đến hệ thống ZK và các thành phần của nó qua minh họa dưới đây.
-
Mạch FV + Hợp đồng thông minh không FV = Bằng chứng kiến thức không không FV
-
Mạch không FV + Hợp đồng thông minh FV = Bằng chứng kiến thức không không FV
-
Mạch FV + Hợp đồng thông minh FV = Bằng chứng kiến thức không FV
Chào mừng tham gia cộng đồng chính thức TechFlow
Nhóm Telegram:https://t.me/TechFlowDaily
Tài khoản Twitter chính thức:https://x.com/TechFlowPost
Tài khoản Twitter tiếng Anh:https://x.com/BlockFlow_News
CertiK
