Phân tích lỗ hổng bảo mật Lean #14576: Khi AI hỗ trợ chứng minh toán học làm lộ khiếm khuyết hệ thống

01-08-2026

Một lỗi về tính đúng đắn (soundness bug) trong kernel của Lean (#14576) đã được báo cáo và khắc phục trong tuần lễ ngày 27 tháng 7. Vấn đề này đã nhận được sự chú ý trên Zulip và các mạng xã hội (ví dụ: X, LinkedIn và Mastodon).

Chuyện gì đã xảy ra

Vào ngày 25 tháng 7, Ramana Kumar đã công bố một kho lưu trữ chứa một "phản chứng" không chứa "sorry" về giả thuyết Collatz, được tạo ra với sự hỗ trợ của AI. Đây không phải là một chứng minh hợp lệ vì nó khai thác một lỗi trong cách kernel xử lý các kiểu quy nạp lồng nhau (nested inductive types). Vào ngày 28 tháng 7, Kiran Gopinathan đã rút gọn nó thành một chứng minh nhỏ về False và mở issue #14576. Chúng tôi đã đẩy bản sửa lỗi một giờ sau khi báo cáo được đưa ra (#14577). Joachim Breitner đã xem xét và đề xuất các cải tiến, sau đó bản sửa lỗi đã được hợp nhất. Các bản phát hành patch mới đã được tung ra.

Về lỗi này: khi kernel loại bỏ một sự xuất hiện lồng nhau dưới một kiểu quy nạp T với các tham số Ds, và các tham số này là phantom (không được đề cập trong các trường của constructor), chúng sẽ biến mất khỏi kiểu phụ trợ được tạo ra và do đó thoát khỏi quá trình kiểm tra kiểu. Một đối số sai kiểu ở vị trí đó có thể được sử dụng để khiến kernel chấp nhận một chứng minh về False. Lỗi này chỉ có thể tiếp cận được thông qua metaprogramming, bằng cách gửi trực tiếp khai báo quy nạp tới kernel. Frontend kiểm tra các đối số và bắt được thuật ngữ sai kiểu đó. Đây là một lỗi thực thi, không phải là lỗ hổng trong meta-theory của Lean.

Tại sao nanoda không phát hiện ra nó

Kho lưu trữ Collatz ban đầu cũng đã vượt qua một phiên bản nanoda cũ một tuần, đây là trình kiểm tra bên ngoài chính. nanoda là một kernel độc lập (hay còn gọi là trình kiểm tra chứng minh/kiểu) cho Lean được Chris Bailey triển khai bằng Rust. Điều đáng ngạc nhiên là có hai lỗi không liên quan cùng tham gia vào sự việc này. Kernel chính thức đã thiếu một bước kiểm tra trong phần hỗ trợ kiểu quy nạp lồng nhau như đã giải thích ở trên. nanoda có kiểm tra điểm đó, nhưng lại không xác minh tên kiểu trong một node projection. Lỗi nanoda đã được Jeremy Chen báo cáo và khắc phục một tuần trước khi lỗi Lean được báo cáo. Chứng minh được xây dựng sao cho biểu thức mà kernel không bao giờ kiểm tra lại chính là biểu thức mà nanoda phiên bản cũ chấp nhận.

Ramana tin rằng thời điểm xảy ra chỉ là trùng hợp, nhưng không thể loại trừ khả năng mô hình đã nhìn thấy báo cáo về nanoda. Joachim đưa ra giả thuyết rằng sự trùng hợp về thời gian là do sự sẵn có của các mô hình mạnh mẽ có khả năng tìm ra lỗi này.

Hệ quả thực tế: việc kiểm tra bằng một kernel độc lập vẫn hiệu quả, vì nó đòi hỏi hai lỗi riêng biệt trong hai bản triển khai, nhưng người dùng dựa vào nó cần cập nhật phiên bản mới nhất của cả hai. lean4lean bị ảnh hưởng bởi lỗi kernel này, vì cách xử lý các kiểu quy nạp của nó là một bản port từ bản triển khai tham chiếu.

Xác minh

lean4lean của Mario Carneiro là một sự hình thức hóa (formalization) Lean của lý thuyết kiểu của Lean cùng với một chứng minh rằng kernel thực thi nó. Công việc này vẫn đang tiếp diễn, chứng minh về tính nhất quán vẫn chưa bao gồm các kiểu quy nạp, và bản triển khai cần được xác minh cũng mắc phải lỗi tương tự như kernel chính thức. Lỗi này lẽ ra đã được tìm thấy khi cố gắng hoàn tất việc xác minh phần này.

Về việc loại bỏ metaprogramming

Một đề xuất trong cuộc thảo luận là loại bỏ hoặc hạn chế metaprogramming để cuộc tấn công này không thể thực hiện được. Điều này là sai lầm. Trình elaborator vốn dĩ không được tin cậy theo thiết kế. Tính đúng đắn không thể phụ thuộc vào một thành phần không đáng tin cậy trong việc từ chối xây dựng một thuật ngữ xấu. Một kẻ tấn công muốn gửi một chứng minh độc hại cũng có thể viết trực tiếp các tệp.olean hoặc sửa đổi bộ nhớ, cả hai cách này đều bỏ qua hoàn toàn trình elaborator. Kernel phải tự mình từ chối các khai báo sai kiểu trong chính tiến trình của nó. Sự tách biệt và cô lập các mối quan tâm này là một trong những ưu điểm chính của các thuật ngữ chứng minh (proof terms).

Những gì FRO đang thực hiện

Các bài kiểm tra hồi quy (regression tests) cho lỗ hổng này, và cho một trường hợp tham số không đồng nhất liên quan do Arthur Adjedj nêu ra, hiện nằm trong Kernel Arena.

Một PR tiếp theo (#14582) yêu cầu kernel kiểm tra xem các tham số của một sự xuất hiện lồng nhau có thực sự hoạt động như các tham số hay không, thay vì chỉ kiểm tra lại kiểu của chúng.

Daniel Selsam tại OpenAI đã hỗ trợ Lean FRO bằng một AI chuyên về an ninh mạng và tìm thấy các lỗi lập trình khác trong kernel của Lean. Tất cả chúng đều đã được khắc phục. Tất cả chúng đều được nanoda bắt được. Những lỗi này cũng chỉ có thể tiếp cận được thông qua metaprogramming. Các PR: #14607, #14608, #14609, #14613, #14615, #14616.

Chúng tôi cũng đã tăng cường các bất biến (invariants) của kernel. Các PR: #14621, #14631, #14632.

comparator.live hiện chạy nanoda theo mặc định, và nanoda được theo dõi hàng ngày để lean-eval và comparator luôn cập nhật sau các bản sửa lỗi từ upstream.

Chúng tôi đang liên hệ và hỗ trợ các chuyên gia có thể tìm thêm lỗi, phát triển các kernel mới và làm việc trên lý thuyết hoặc trên các kernel đã được xác minh.

Lời cảm ơn

Tôi rất biết ơn Joachim Breitner và Sebastian Ullrich vì những chỉnh sửa và đề xuất của họ cho bài viết này.