AI tự động tìm ra 7 lỗ hổng bảo mật nghiêm trọng trong thư viện mật mã của Cloudflare

Chúng tôi đã hướng đường ống kiểm định AI của mình vào thư viện mật mã thực nghiệm CIRCL của Cloudflare và xác nhận bảy lỗi thực tế, từ lỗi mất độ chính xác float64 nghiêm trọng trong threshold RSA cho đến việc phá vỡ hoàn toàn kiểm soát truy cập trong mã hóa dựa trên thuộc tính (attribute-based encryption). Tất cả bảy lỗi hiện đã được khắc phục ở bản gốc (upstream). Đây là bài viết đầu tiên trong loạt bài về các lỗi mà các tác nhân (agents) của chúng tôi tìm thấy trong các dự án mật mã nguồn mở.

Tại zkSecurity, chúng tôi đang xây dựng zkao, một tác nhân kiểm định AI. Mục tiêu rất đơn giản để nêu ra nhưng lại khó thực hiện: giữ cho AI liên tục giám sát mã nguồn của bạn cho đến khi không còn lỗi nào mà các công cụ AI khác có thể tìm thấy. Chúng tôi đã viết về lý do tại sao cách tiếp cận đó lại quan trọng trong bài: zkao: Bảo mật tích lũy (Security That Compounds).

Việc xây dựng zkao là một quá trình lặp đi lặp lại, với mục tiêu cuối cùng là tạo ra một kiểm định viên tự động có khả năng tìm thấy tất cả các lỗi mà AI có thể phát hiện. Quá trình này bao gồm việc động não các ý tưởng và kỹ thuật mới, mã hóa một cách hệ thống chuyên môn của các nhà nghiên cứu bảo mật tại zkSecurity vào zkao, đảm bảo rằng nó phát hiện được các lỗ hổng mới nhất và nghiêm trọng nhất mà không bị thiên kiến đối với các bộ tiêu chuẩn (benchmarks), và quan trọng hơn là liên tục thực hiện các thử nghiệm để hiểu điều gì hiệu quả, điều gì không, cách các mô hình tiến hóa, và để làm sâu sắc thêm hiểu biết của chúng tôi về việc tìm lỗi bằng AI. Một số thử nghiệm trong đó tạo ra những kết quả đáng chia sẻ độc lập với sản phẩm, và đó chính là nội dung của loạt bài viết này.

Ngoài ra còn có một động lực thứ hai. Những thử nghiệm này là cách chúng tôi xây dựng một bộ tiêu chuẩn (benchmark suite) cho zkao, và trong quá trình đó, chúng liên tục làm sáng tỏ cách các LLM thực sự suy luận về mật mã: đâu là điểm sắc bén, đâu là điểm mù, và làm thế nào để khuếch đại điểm mạnh và hạn chế điểm yếu. Mặc dù các lỗi là kết quả đầu ra có thể nhìn thấy được, nhưng các mô hình suy luận mới là phần chúng tôi quan tâm nhất.

Vài tháng trước, chúng tôi bắt đầu thực hiện các thử nghiệm trên các cơ sở mã (codebases) được chọn lọc. Chúng tôi đã sử dụng các LLM để quét một vài dự án mật mã nguồn mở, theo hai cấu hình:

Chỉ dùng LLM, với một câu lệnh (prompt) đơn giản.

LLM có kỹ năng (skills), trong đó các kỹ năng được duy trì bởi các chuyên gia trong nhóm của chúng tôi.

Sau đó, đối với các dự án quan trọng nơi các LLM tìm thấy lỗ hổng thực tế, chúng tôi cũng chạy zkao để xem liệu nó có thể tự phát hiện ra các vấn đề tương tự hay không. Trong hầu hết các trường hợp, zkao không chỉ tìm thấy tất cả các lỗi đó mà còn xác định được những lỗi phức tạp và nghiêm trọng hơn.

Kết quả tốt đến mức chúng tôi quyết định viết thành bài. Chúng tôi bắt đầu loạt bài này với CIRCL của Cloudflare, một thư viện mật mã nâng cao và hậu lượng tử (post-quantum cryptography). Trên CIRCL, đường ống của chúng tôi đã tạo ra nhiều kết quả tiềm năng, và bảy trong số đó đáng để báo cáo tại đây. Tất cả bảy lỗi hiện đã được khắc phục ở bản gốc. Hầu hết chúng đã được xác nhận và trao thưởng thông qua chương trình của Cloudflare trên HackerOne.

Làm rõ: AI chỉ tạo ra các kết quả tiềm năng, không phải báo cáo cuối cùng. Con người trong nhóm của chúng tôi vẫn xác thực từng vấn đề, kiểm tra khả năng khai thác, tối giản hóa POC (Proof of Concept) khi cần thiết và xử lý việc công bố. Bước có sự tham gia của con người (human-in-the-loop) đó vẫn rất quan trọng, vì các kết quả tiềm năng từ AI thì rẻ, trong khi các báo cáo đáng tin cậy thì không.

Tối giản hóa bước đó là một trong những mục tiêu chính mà zkao được xây dựng để thực hiện, và mặc dù vẫn đang trong quá trình hoàn thiện, phiên bản hiện tại đã tự đảm nhận phần lớn công việc xác thực này.

Tổng quan về mức độ nghiêm trọng và các bản sửa lỗi

Một điều cần lưu ý trước khi đi vào chi tiết: mức độ nghiêm trọng mà AI tự gán cho kết quả của nó thường không chính xác (noisy). Dưới đây là từng lỗi theo đánh giá của AI và theo xác nhận của Cloudflare sau khi đã khắc phục. Chúng tôi cũng đã kiểm tra để đảm bảo cả bảy lỗi đều có thể tái lập một cách nhất quán bởi phiên bản zkao hiện tại.

Khoảng cách giữa mức độ nghiêm trọng do AI đánh giá và mức độ nghiêm trọng được xác nhận là một thông tin thú vị, và chúng tôi sẽ quay lại vấn đề này ở phần cuối. Bây giờ là bảy lỗi, từng lỗi một.

Lỗi 1: đánh giá đa thức trong float64

Lỗi này nằm trong triển khai threshold RSA của CIRCL (tss/rsa). Việc ký ngưỡng (threshold signing) chia sẻ một bí mật cho n người chơi bằng cách sử dụng chia sẻ bí mật kiểu Shamir. Hàm Deal() đánh giá một đa thức bí mật tại chỉ số của mỗi người chơi. Các hệ số là big.Int, như lẽ ra phải thế, nhưng số hạng $x^i$ lại được tính như sau:

float64 có phần định trị (mantissa) 53-bit. Ngay khi $x^i$ vượt quá $2^{53}$ (khoảng $9 \times 10^{15}$), kết quả sẽ bị làm tròn âm thầm trước khi được ép kiểu trở lại thành số nguyên. Ví dụ, với 100 người chơi và ngưỡng là 27, việc đánh giá tại $x = 100$ với $i = 26$ sẽ yêu cầu $100^{26} = 10^{52}$, vượt quá $2^{53}$ tới 36 bậc độ lớn. Ngay cả $x = 20, i = 16$ cũng đã gây ra lỗi này.

Hệ quả là đa thức được đánh giá không chính xác, dẫn đến các phần chia sẻ khóa (key shares) được trao cho người chơi bị sai. Tùy thuộc vào các tham số, việc kết hợp chữ ký sẽ thất bại hoàn toàn hoặc tạo ra các phần chia sẻ trông có vẻ ổn nhưng không thể khôi phục lại khóa dự định. Tác nhân của chúng tôi đã gắn cờ đây là lỗi nghiêm trọng, vì nó dẫn đến việc tạo ra các phần chia sẻ khóa không chính xác, làm tổn hại đến tính đúng đắn của giao thức. Cloudflare cuối cùng đã đánh giá vấn đề này ở mức độ nghiêm trọng Thấp, dựa trên khả năng xảy ra thấp của các điều kiện bị ảnh hưởng trong thực tế.

Bản sửa lỗi thay thế phép lũy thừa dấu phẩy động bằng phương pháp đánh giá Horner mà chính bình luận TODO trong mã nguồn đã gợi ý từ trước, giữ mọi thứ ở định dạng big.Int. Commit f7d2180.

Lỗi 2: giả mạo bằng chứng DLEQ thông qua tham số bảo mật do người chứng minh kiểm soát

Lỗi này nằm trong zk/qndleq, bằng chứng DLEQ (đẳng thức logarit rời rạc) của CIRCL cho nhóm con các số chính phương trong $(\mathbb{Z}/n\mathbb{Z})^*$. Một bằng chứng DLEQ chứng thực rằng hai cặp chia sẻ cùng một logarit rời rạc; nếu kẻ tấn công có thể khiến người xác minh chấp nhận một bằng chứng cho một tuyên bố sai, hệ thống bằng chứng đó đã bị phá vỡ.

Thử thách (challenge) trong bằng chứng này được dẫn xuất theo kiểu Fiat-Shamir, và độ dài bit của nó được quy định bởi một SecParam. Vấn đề là SecParam nằm ngay bên trong cấu trúc Proof:

Trong quá trình xác minh, mã nguồn tính toán lại thử thách bằng cách sử dụng chính SecParam của bằng chứng. Trường đó do kẻ tấn công kiểm soát. Nếu đặt SecParam = 1, thử thách sẽ thu gọn thành một bit duy nhất, giá trị 0 hoặc 1: giống như tung đồng xu cho mỗi lần thử giả mạo. Nếu đặt SecParam = 8, việc brute force chỉ mất khoảng $2^8 = 256$ lần thử. Dù thế nào đi nữa, tính đúng đắn (soundness) đã mất.

Đây là một ví dụ rõ ràng về một mô hình lặp đi lặp lại: một tham số bảo mật phải được cố định bởi người xác minh thay vì được đọc từ dữ liệu do người chứng minh cung cấp. Bản sửa lỗi loại bỏ SecParam khỏi bằng chứng và yêu cầu hàm Verify nhận nó như một đối số tường minh, để người xác minh thiết lập nó. Commit 757dde4.

Lỗi 3: xác minh tổng hợp BLS mà không kiểm tra tính phân biệt của thông điệp

Đây là lỗi duy nhất trong nhóm mà AI đánh giá thấp. Tác nhân đã gắn nhãn nó là trung bình. Thực tế, đây là một cuộc tấn công khóa giả (rogue key attack) kinh điển, một lỗ hổng cấp độ nghiêm trọng đã được biết đến rộng rãi; chúng tôi đã báo cáo nó là nghiêm trọng, và Cloudflare xác nhận nó ở mức cao.

VerifyAggregate trong sign/bls triển khai chế độ tổng hợp BLS BASIC. Chế độ đó chỉ an toàn nếu tất cả các thông điệp trong lô (batch) là riêng biệt, đó là cơ chế phòng thủ chống lại các cuộc tấn công khóa giả. Hàm này đã kiểm tra phương trình ghép cặp tổng hợp nhưng không bao giờ kiểm tra xem các thông điệp có riêng biệt hay không, để lại yêu cầu quan trọng đó cho người gọi.

Nếu không có nó, cuộc tấn công khóa giả tiêu chuẩn sẽ xảy ra. Một kẻ tấn công nhìn thấy khóa công khai $\mathsf{pk}_v$ của nạn nhân và một thông điệp $m$ có thể đăng ký $\mathsf{pk}_a = g^{\mathsf{sk}_a} - \mathsf{pk}_v$ và giả mạo một chữ ký tổng hợp trên $(\mathsf{pk}_v, m)$ và $(\mathsf{pk}_a, m)$ mà không cần biết khóa bí mật của nạn nhân. CIRCL không cung cấp cơ sở hạ tầng chứng minh quyền sở hữu (proof-of-possession) để dự phòng, điều này làm cho việc thiếu kiểm tra trở nên nguy hiểm hơn.

Tại sao AI lại gọi đây là mức trung bình? Chúng tôi không biết. Đọc phần suy luận của nó, nó đã phát hiện chính xác việc thiếu kiểm tra tính phân biệt và thậm chí còn gọi tên cuộc tấn công khóa giả, nhưng sau đó nó lại bám vào thực tế là hợp đồng của chế độ BASIC đặt yêu cầu phân biệt lên người gọi. Nó coi "người gọi phải xử lý việc này" như một biện pháp giảm thiểu và hạ mức độ nghiêm trọng xuống.

Bản sửa lỗi khiến VerifyAggregate từ chối các lô được tạo với các thông điệp trùng lặp. Commit 9798df7.

Lỗi 4: phá vỡ tính đúng đắn của DLEQ thông qua xung đột dấu trong FillBytes

Quay lại zk/qndleq cho lỗi tinh vi nhất, và thẳng thắn mà nói là thú vị nhất trong nhóm. Nó không yêu cầu phải chạm vào bằng chứng chút nào.

Lấy một bằng chứng pi trung thực, hợp lệ cho tuyên bố $S_1 = (g, g_x, h, h_x)$, chứng thực rằng $\log_g(g_x) = \log_h(h_x) = x$. Một kẻ tấn công không biết $x$ sẽ trình bày chính pi đó cho người xác minh, nhưng ghép nó với một tuyên bố khác, $S_2 = (g, -g_x, h, h_x)$, trong đó $-g_x$ là số big.Int âm new(big.Int).Neg(gx).

Tuyên bố giả mạo được chấp nhận bất cứ khi nào thử thách $c$ là số chẵn, vì hai thứ khớp nhau cùng một lúc.

Triệt tiêu đại số. Người xác minh tính toán lại giá trị của nó từ $-g_x$, và các hệ số dấu bị triệt tiêu trực tiếp:

$$(-g_x)^c \bmod N = (N - g_x)^c \bmod N = (-1)^c \cdot g_x^c \bmod N.$$

Khi $c$ là số chẵn, $(-1)^c = 1$, vì vậy người xác minh tái tạo chính xác các giá trị trung gian giống như người chứng minh trung thực đã làm.

Xung đột dấu trong hàm băm. Thử thách được dẫn xuất bằng cách băm tuyên bố, và việc băm sử dụng FillBytes, vốn ghi giá trị tuyệt đối của một big.Int và loại bỏ dấu. Vì vậy, doChallenge(..., -gx, ...) và doChallenge(..., gx, ...) băm ra cùng một kết quả.

Ở đây, $c$ là số chẵn với xác suất ít nhất là 1/2 (nó chỉ là bit thấp của đầu ra hàm băm), vì vậy cuộc tấn công thành công trên khoảng một nửa số bằng chứng được tạo ra một cách trung thực. Người xác minh tin rằng $\log_g(-g_x) = \log_h(h_x)$, điều này là sai. Đây là cốt lõi của bằng chứng khái niệm (proof-of-concept):

Điều làm cho lỗi này nổi bật là nó không phải là một dòng mã cẩu thả đơn lẻ. Đó là sự tương tác giữa một đẳng thức đại số ($(-1)^{\text{chẵn}} = 1$) và một lựa chọn tuần tự hóa trông có vẻ vô hại (FillBytes loại bỏ dấu). Không cái nào sai khi đứng riêng lẻ. Nhưng khi kết hợp lại, chúng phá vỡ tính đúng đắn. Suy luận qua loại ranh giới đó chính là nơi chúng tôi ngạc nhiên nhất về những gì các mô hình phát hiện ra.