Trong thế giới tiền điện tử đầy phức tạp, việc đảm bảo an ninh cho các hệ thống blockchain là vô cùng quan trọng. Một dự án nổi bật trong lĩnh vực này là Axiom, một hệ thống cho phép tính toán trên toàn bộ lịch sử của Ethereum. Điều đặc biệt là mọi tính toán này đều được xác minh bằng các bằng chứng không kiến thức (zero-knowledge proofs – ZKPs) ngay trên chuỗi khối (on-chain), sử dụng các phép toán SNARK và đường cong elliptic đã được ZK xác minh.

Để xây dựng hệ thống này, Axiom đã sử dụng Halo2, một framework phức tạp. Việc sử dụng Halo2 đòi hỏi phải đối mặt với nhiều thách thức, đặc biệt là các vấn đề tiềm ẩn liên quan đến việc thiếu ràng buộc (under-constrained) do API cấp thấp của nó.

Bài viết này sẽ giúp bạn hiểu rõ hơn về quy trình đánh giá bảo mật của Axiom, những lỗi được phát hiện (bao gồm cả các lỗi nghiêm trọng có thể phá vỡ tính bảo mật của hệ thống), và các biện pháp mà Axiom đã thực hiện để khắc phục những vấn đề này.

Hệ thống Axiom hoạt động như thế nào?

Axiom được thiết kế để cung cấp quyền truy cập vào dữ liệu lịch sử của blockchain cho các ứng dụng EVM (Ethereum Virtual Machine). Thông thường, các hợp đồng EVM chỉ có thể truy cập trạng thái tài khoản hiện tại của chính chúng, chứ không thể xem các trạng thái trước đây, trạng thái giao dịch hoặc trạng thái của các tài khoản khác.

Để giải quyết vấn đề này, Axiom sử dụng ZKPs để xác minh một cách ngắn gọn các truy vấn linh hoạt trên các giao dịch và trạng thái lịch sử. Cụ thể, họ sử dụng framework Halo2 ZKP để cho phép người dùng đọc và tin tưởng dữ liệu lịch sử, chẳng hạn như tiêu đề, trạng thái và giao dịch.

Để xây dựng một hệ thống như vậy, Axiom phải mô hình hóa dữ liệu, giao dịch, trạng thái, v.v. của Ethereum bằng các mạch Halo2. Điều này đòi hỏi việc viết các mạch Halo2 cho các thành phần cơ bản cấp thấp, chẳng hạn như mật mã đường cong elliptic, cũng như các cấu trúc dữ liệu cấp cao hơn, như cây Merkle và các khối Ethereum. Vì các thư viện mạch Halo2 hiện có rất hạn chế, nên nhiều thành phần cơ bản trong số này phải được phát triển như một phần của thư viện `halo2-base` và `halo2-ecc` của Axiom và được sử dụng trong thư viện `snark-verifier` để đệ quy SNARK. Ngoài các thư viện cấp thấp tùy chỉnh, Axiom còn sử dụng phiên bản sửa đổi của chính hệ thống chứng minh Halo2. Một số mạch Axiom bao gồm bằng chứng về các mảng có độ dài thay đổi, được hưởng lợi rất nhiều từ các mạch đa pha, được triển khai như một tính năng thử nghiệm trong nhánh Halo2 của Privacy & Scaling Explorations.

Axiom lưu ý rằng kể từ khi quá trình kiểm tra kết thúc, họ đã ngừng sản phẩm bộ đồng xử lý ZK mà các mạch ZK ban đầu dự định sử dụng và Axiom hiện đang sử dụng chúng làm phần phụ thuộc trong dự án OpenVM, một máy ảo dựa trên ZK mô-đun và hiệu suất cao cho phép các crate Rust `tùy ý` được sử dụng trong các ứng dụng ZK với một số hạn chế.

Quá trình đánh giá bảo mật

Nhóm mật mã của Trail of Bits đã làm việc để xem xét các mạch Halo2 của Axiom qua hai đánh giá riêng biệt. Dự án đầu tiên của chúng tôi, kéo dài từ ngày 10 tháng 2 đến ngày 17 tháng 5 năm 2023, tập trung vào các nguyên thủy Halo2 cấp thấp (nhánh Halo2 của PSE), chẳng hạn như số học đường cong elliptic và các hàm băm, cũng như một số logic nghiệp vụ của Axiom. Đợt kiểm tra thứ hai, kéo dài từ ngày 11 tháng 9 đến ngày 29 tháng 9 năm 2023, tập trung vào các thay đổi/nâng cấp của Axiom so với đánh giá đầu tiên cũng như đánh giá sâu hơn về logic xác minh SNARK.

Do tính chất của các dự án này, phần lớn nỗ lực của chúng tôi bao gồm việc xem xét thủ công sâu các mạch Halo2. May mắn thay, nhóm mật mã của chúng tôi đã xem xét nhiều dự án sử dụng framework Halo2, và vì vậy chúng tôi duy trì các ghi chú và tài liệu nội bộ liên quan đến các điểm khó và cạm bẫy phổ biến liên quan đến các ứng dụng Halo2, mà chúng tôi đã tận dụng (và cập nhật) liên tục trong suốt các dự án với Axiom. Việc xem xét hiệu quả hệ thống này đòi hỏi chúng tôi phải nghiên cứu rộng rãi hệ thống Axiom bằng cách xem xét tài liệu của họ và duy trì một cuộc đối thoại cởi mở với các kỹ sư Axiom thông qua Slack và các cuộc gọi hàng tuần.

Mặc dù các dự án này chủ yếu là nỗ lực thủ công, nhưng chúng tôi đã tận dụng các công cụ để tự động hóa một số phân tích của mình. Chúng tôi đã sử dụng một số công cụ tiện ích Rust như cargo-audit và Clippy để tìm các phụ thuộc đã lỗi thời và các sự cố Rust phổ biến, đồng thời chúng tôi đã sử dụng Semgrep để tìm các sự cố Rust phổ biến hơn và các sự cố logic cụ thể của Axiom. Sử dụng Semgrep, chúng tôi đã có thể phát triển các phân tích tùy chỉnh nhắm mục tiêu vào Halo2; cụ thể, khi chúng tôi xác định được sự cố bảo mật Halo2 có thể xuất hiện ở các vị trí khác, chúng tôi đã sử dụng Semgrep để thực hiện phân tích biến thể và xác định cũng như khắc phục tất cả các sự cố tương tự.

Những khó khăn khi đánh giá Halo2

Để tạo ZKP chứng minh việc thực thi một chương trình cụ thể, người ta phải mô hình hóa chương trình ở định dạng (mạch) mà hệ thống ZKP có thể sử dụng. Halo2 (và những hệ thống khác như Circom, Cairo và Noir) là một thư viện được nhóm ZCash phát triển cho phép bạn thực hiện chính xác điều đó; cụ thể, nó cho phép bạn chỉ định các mạch bao gồm các phương trình đa thức được kích hoạt có chọn lọc được gọi là “cổng”, các ràng buộc đẳng thức hoạt động như “dây” giữa các cổng đó và các ràng buộc bao gồm tập hợp con được gọi là “tra cứu”. Về cơ bản, mạch của bạn là một hệ thống phương trình khổng lồ, trong đó mỗi phương trình là một trong một số phương trình “cổng” cụ thể, có thể có các giá trị hằng số khác nhau. Các biến trong các phương trình này đại diện cho các giá trị khác nhau được sử dụng trong suốt quá trình tính toán, chẳng hạn như đầu vào, giá trị trung gian và đầu ra của bạn. Kiểu định nghĩa mạch này được gọi là “plonkish”, vì nó tổng quát hóa loại mạch số học cổng và dây lần đầu tiên được phổ biến bởi hệ thống chứng minh PLoNK. Thay vì trực tiếp tính toán kết quả, các mạch thường _kiểm tra_ xem tất cả các giá trị này có khớp với quá trình thực thi chính xác của chương trình của bạn hay không. Các chi tiết đầy đủ phức tạp hơn nhiều, nhưng nếu bạn tò mò, bạn có thể xem sách Halo2.

Một trong những lớp lỗi phổ biến và nghiêm trọng nhất đối với các mạch ZKP được gọi là lỗi âm thanh “ít ràng buộc”. Một biến trong mạch bị ràng buộc thấp khi nó có thể nhận nhiều giá trị có thể, một số trong số đó vi phạm các giả định của phần còn lại của mạch. Điều này thường xảy ra khi một phép tính trực tiếp được thay thế bằng một kiểm tra. Ví dụ: nếu bạn chạy `x = sqrt(9)` trong một chương trình bình thường, `x` sẽ luôn bằng một giá trị, thường là 3. Tuy nhiên, nếu bạn thay thế điều này trong một mạch bằng một kiểm tra hiệu quả hơn (tức là thay vì trực tiếp tính toán `x`, thay vào đó bạn hãy để người chứng minh chọn một số giá trị cho `x` và sau đó bạn kiểm tra xem `x^2 == 9`), thì một người chứng minh độc hại có thể chọn đặt `x` thành 3 hoặc -3. Đôi khi, sự linh hoạt này không thể khai thác được—nhưng trong những trường hợp nghiêm trọng, một người chứng minh độc hại về cơ bản có thể tạo ra các bằng chứng giả, nơi họ thực hiện các phép tính không chính xác hoặc không hợp lệ một cách sai lầm, nhưng họ vẫn tạo ra một ZKP xác minh là chính xác.

Halo2 cung cấp một API cấp thấp để xác định các mạch. Điều này cho phép các nhóm phát triển các tập hợp ràng buộc được điều chỉnh theo yêu cầu tùy chỉnh cho phép họ tối ưu hóa cho các nhu cầu cụ thể của họ và đạt được hiệu suất tốt hơn nhiều để tạo ZKP. Tuy nhiên, đây là một con dao hai lưỡi, vì mỗi loại ràng buộc cũng giới thiệu những nguy hiểm mới và sự tương tác của các ràng buộc khác nhau có thể khiến việc đưa ra các lỗ hổng bảo mật dễ dàng hơn nhiều. Chúng tôi đặc biệt tìm thấy các lỗi “ít ràng buộc” trong các mạch có các loại dữ liệu khác nhau. Vì mỗi biến trong mạch Halo2 là một phần tử trường hữu hạn, nên người triển khai cần tung hứng nhiều ràng buộc bổ sung để đảm bảo rằng các biến có một tập hợp giá trị hạn chế hơn—ví dụ: các biến đại diện cho giá trị chân lý chỉ là 0 hoặc 1. Vì mỗi ràng buộc đều tốn kém, nên người triển khai cố gắng tránh các ràng buộc dư thừa, nhưng đôi khi lý do có thể bỏ qua một ràng buộc được trải rộng trên hàng tá tệp và hàng nghìn dòng mã, và những sai lầm có thể cực kỳ khó nhận thấy.

Có một số tài nguyên tốt để học Halo2, chẳng hạn như sách Halo2, nhưng chúng có những hạn chế. Cụ thể, nếu bạn mở sách Halo2, bạn sẽ nhận thấy có khá nhiều TODO (và thậm chí còn có nhiều hơn khi chúng tôi làm việc với Axiom). Ngoài ra, khi bạn bắt đầu tìm hiểu sâu về Halo2, bạn sẽ nhanh chóng nhận thấy rằng có rất nhiều điểm khó, đó là lý do tại sao chúng tôi cảm thấy cần phải duy trì tài liệu và hướng dẫn nội bộ để sử dụng Halo2. Để cung cấp cho bạn một cảm giác về điều này, đây là một vài ghi chú được lấy từ tài liệu nội bộ của chúng tôi:

• Ký hiệu API có thể không nhất quán. Cụ thể, `Region::assign_advice` không tạo ràng buộc, nhưng `Region::assign_advice_from_instance` và `Region::assign_advice_from_constant` thì có tạo ràng buộc. Nếu bạn trộn lẫn chúng và nghĩ rằng `Region::assign_advice` gán một ràng buộc, bạn có thể đã giới thiệu một lỗi ít ràng buộc nghiêm trọng.

• Ràng buộc thích hợp yêu cầu nhiều lệnh gọi API. Các ràng buộc sao chép, cho phép bạn sao chép các giá trị trong mạch, được giới thiệu bằng một lệnh gọi tới `AssignedCell::copy_advice`. Tuy nhiên, để thực thi thực tế các ràng buộc sao chép, bạn cần bật kiểm tra hoán vị cho các cột đã cho bằng một lệnh gọi tới `ConstraintSystem::enable_equality`.

Chúng tôi có toàn bộ danh sách các ghi chú tương tự như những ghi chú đó. Hãy nhớ rằng hỗ trợ công cụ cho Halo2 là cực kỳ hạn chế, và vì vậy việc xác minh tất cả những điểm tinh tế này là một quá trình chủ yếu thủ công.

Những phát hiện quan trọng

Hai đánh giá bảo mật của chúng tôi về các mạch Axiom Halo2 đã xác định tổng cộng 35 sự cố bảo mật. Trong số này, có bốn sự cố có mức độ nghiêm trọng cao và liên quan đến các vấn đề về âm thanh hoặc ít ràng buộc, có khả năng phá vỡ toàn bộ bảo mật của hệ thống. Dưới đây là tóm tắt nhanh về bốn vấn đề này:

• TOB-AXIOM-3: Mạch `idx_to_indicator` bị ràng buộc thấp. Mạch này được cho là xuất ra một vectơ gồm tất cả các số không và số một, trong đó mọi phần tử trong vectơ đều bằng không, ngoại trừ vị trí của `idx`, được cho là bằng một. Do thiếu một ràng buộc, vectơ gồm tất cả các số không sẽ luôn được coi là một câu trả lời đúng và do đó, một người chứng minh độc hại có thể chèn giá trị này và tạo ra các phép tính không chính xác sẽ được xác minh là đúng.

• TOB-AXIOM-13: Hai trong số các mạch nhân vô hướng có thể trả về kết quả bị ràng buộc thấp. Nếu bị khai thác, điều này có thể cho phép một người chứng minh độc hại tạo ra các kết quả nhân vô hướng không chính xác sẽ được coi là hợp lệ. Điều này có thể có ý nghĩa đối với các hoạt động như xác minh chữ ký (tức là giả mạo chữ ký) sử dụng các hoạt động này.

• TOB-AXIOM-19: Một lỗi chính tả nhỏ nhưng tai hại trong hàm `assert_equal` có nghĩa là nó không thực sự khẳng định sự bằng nhau. Về cơ bản, hàm này được cho là so sánh hai giá trị với nhau để xem chúng có bằng nhau hay không, nhưng thay vào đó nó so sánh giá trị đầu tiên với chính nó. Sai lầm nhỏ này có thể gây ra hậu quả nghiêm trọng vì hàm này được sử dụng ở nhiều vị trí quan trọng, chẳng hạn như xác minh bằng chứng và điều này sẽ phá vỡ tính hợp lệ của bằng chứng.

• TOB-AXIOMv2-3: Phương thức `range_check` được cho là giới hạn một giá trị số nguyên nằm dưới một phạm vi nhất định, nhưng điều này đã được thực thi bằng `debug_assert`, thay vì một ràng buộc thực tế. Điều này có nghĩa là các giá trị lớn sẽ bị bắt trong quá trình thử nghiệm, nhưng sau khi triển khai, một người chứng minh độc hại có thể tạo ra các giá trị độc hại và điều này sẽ không bị ZKP bắt. May mắn thay, dựa trên cách nó được sử dụng, nó không thể khai thác được trong hệ thống Axiom, nhưng nó có thể gây ra vấn đề nếu nó được sử dụng theo những cách khác.

Các phát hiện đáng chú ý khác bao gồm việc xử lý không chính xác các trường hợp đặc biệt như điểm ở vô cực trong các hoạt động đường cong elliptic và các khu vực mà các giả định nguy hiểm có thể gây ra các lỗ hổng hệ thống.

Ngoài những vấn đề bảo mật này, chúng tôi cũng nêu ra một số vấn đề mà chúng tôi gọi là vấn đề về chất lượng mã. Bản thân những vấn đề này không đại diện cho các vấn đề bảo mật ngay lập tức, nhưng chúng tôi vẫn nêu ra chúng vì chúng có thể dẫn đến các vấn đề bảo mật sau này hoặc đại diện cho các cơ hội để làm cho cơ sở mã dễ đọc hoặc hiệu quả hơn. Trong cả hai đánh giá, chúng tôi đã nêu ra tổng cộng 25 vấn đề về chất lượng mã liên quan đến các mối lo ngại như nhận xét không chính xác và các lệnh gọi Rust dư thừa.

Đề xuất: con đường phía trước

Khi chúng tôi làm việc với Axiom, họ còn khá sớm trong vòng đời phát triển của mình. Đặc biệt, các mạch Halo2 mà chúng tôi đã xem xét trong dự án đầu tiên của mình mới chỉ được phát triển gần đây vào thời điểm đó và sau dự án này, Axiom tiếp tục phát triển các mạch bổ sung, mà chúng tôi đã xem xét trong đánh giá thứ hai. Đây là lý do tại sao, khi bạn đọc báo cáo bảo mật của chúng tôi, bạn sẽ thấy rằng Đánh giá độ hoàn thiện của cơ sở mã của chúng tôi đã cho Axiom xếp hạng thấp nhất của chúng tôi là yếu/thiếu trong các lĩnh vực như tài liệu và thử nghiệm.

Mặc dù tài liệu và thử nghiệm là điều cần thiết cho bất kỳ dự án quan trọng nào về bảo mật, nhưng điều này đặc biệt đúng khi đối phó với một framework cấp thấp, phức tạp có nhiều điểm khó, như Halo2. Cả thử nghiệm và tài liệu đều là tối quan trọng vì một vài lý do, chẳng hạn như khả năng đọc/kiểm tra tốt hơn, ngăn ngừa hồi quy và xác nhận các hành vi dự kiến. Đây là lý do tại sao, sau cả hai đánh giá của chúng tôi, chúng tôi đã đưa ra cho Axiom các đề xuất chiến lược, dài hạn để cải thiện cả thử nghiệm và tài liệu của họ, ngoài các đề xuất để khắc phục 35 vấn đề mà chúng tôi đã báo cáo.

Chúng tôi rất vui khi thấy rằng Axiom đã lắng nghe những đề xuất này và phản hồi bằng những cải tiến đáng kể trên cả hai mặt trận. Họ đã phát triển một bộ thử nghiệm đầu cuối giữa đánh giá đầu tiên và thứ hai của chúng tôi và mở rộng bộ thử nghiệm sau khi hoàn thành cả hai cuộc kiểm tra.

Tóm lại

Sự hợp tác của chúng tôi với Axiom là một ví dụ tuyệt vời về những thách thức trong việc xây dựng các ứng dụng bằng Halo2, cam kết cần thiết để bảo mật chúng đúng cách và lý do tại sao các đánh giá bảo mật là một phần thiết yếu của chu kỳ phát triển. Đặc biệt, bằng cách tham gia với chúng tôi sớm trong vòng đời phát triển, Axiom đã có thể thực hiện những cải tiến lâu dài, có tác động rất lớn đối với tư thế bảo mật của họ. Điều này rất giống với tác động mà chúng tôi đã thấy với Ockam trong đánh giá thiết kế hệ thống của họ.

Chúng tôi xin cảm ơn một lần nữa nhóm Axiom vì công việc tuyệt vời của họ trong dự án này; họ đã rất hợp tác, phản hồi nhanh và tích cực kết hợp những hiểu biết sâu sắc của chúng tôi sau khi các dự án của chúng tôi hoàn thành. Nếu bạn đang xây dựng một hệ thống mật mã phức tạp như của Axiom và cần hỗ trợ bảo mật, vui lòng liên hệ với nhóm mật mã của chúng tôi!

Giải thích thuật ngữ

• Zero-knowledge proofs (ZKPs): Bằng chứng không kiến thức, cho phép chứng minh một điều gì đó là đúng mà không cần tiết lộ bất kỳ thông tin nào khác ngoài sự thật đó.
• SNARK: Một loại bằng chứng mật mã ngắn gọn, không tương tác, có thể được xác minh nhanh chóng.
• EVM (Ethereum Virtual Machine): Máy ảo Ethereum, môi trường thực thi cho các hợp đồng thông minh trên blockchain Ethereum.
• Halo2: Một framework để xây dựng các hệ thống ZKP, cho phép tạo ra các bằng chứng về tính đúng đắn của các tính toán.
• Under-constrained: Thiếu ràng buộc, một tình trạng trong đó một biến có thể có nhiều giá trị khác nhau, dẫn đến các lỗ hổng bảo mật tiềm ẩn.
• Elliptic curve cryptography: Mật mã đường cong elliptic, một phương pháp mật mã dựa trên các đường cong elliptic trên các trường hữu hạn.
• Merkle tree: Cây Merkle, một cấu trúc dữ liệu được sử dụng để xác minh tính toàn vẹn của dữ liệu.