Lean đã chứng minh chương trình này hoàn toàn chính xác, nhưng tôi vẫn tìm ra lỗi

Các tác nhân AI ngày càng trở nên điêu luyện trong việc phát hiện lỗ hổng bảo mật trong các hệ thống phần mềm quy mô lớn. Trước làn sóng này, kiểm chứng hình thức (formal verification) đang được xem là một giải pháp tiềm năng để xây dựng phần mềm vững chắc. Gần đây, dự án lean-zip — một bản cài đặt thư viện nén zlib được xây dựng và chứng minh tính đúng đắn bởi 10 tác nhân AI sử dụng ngôn ngữ Lean — đã được coi là một cột mốc ấn tượng.

Mô tả dự án lean-zip

Leo De Moura, kiến trúc sư trưởng của Lean FRO, từng khẳng định rằng lean-zip không chỉ là một bản cài đặt bình thường, mà là một phiên bản được kiểm chứng "đầu đến cuối", đảm bảo hoàn toàn không có lỗi triển khai. Tuy nhiên, câu hỏi đặt ra là: Liệu sự "đúng đắn" này có tuyệt đối?

Để kiểm chứng, tôi đã sử dụng một tác nhân Claude kết hợp với các công cụ fuzzing như AFL++, AddressSanitizer và Valgrind để "tấn công" vào lean-zip. Quá trình này đã thực hiện hơn 105 triệu lần thực thi fuzzing trong suốt một cuối tuần.

Kết quả kiểm thử

Kết quả thu được khá thú vị. Trong mã ứng dụng Lean được kiểm chứng, không tìm thấy bất kỳ lỗ hổng bộ nhớ nào. Tuy nhiên, quá trình này đã phát hiện ra hai vấn đề nghiêm trọng nằm ngoài phạm vi của các định lý chứng minh:

1. Lỗi tràn bộ nhớ Heap trong Lean Runtime: Một lỗi tràn bộ nhớ nghiêm trọng trong hàm lean_alloc_sarray của runtime Lean 4, ảnh hưởng đến mọi phiên bản Lean tính đến thời điểm hiện tại.
2. Từ chối dịch vụ (DoS) trong trình phân tích cú pháp: Một lỗi khiến chương trình bị treo do hết bộ nhớ (OOM) khi xử lý các tệp nén có kích thước header bị giả mạo.

Lỗi tràn bộ nhớ trong Runtime

Đây là phát hiện đáng báo động nhất. Lỗi nằm trong hàm lean_alloc_sarray — một phần của Cơ sở tính toán tin cậy (Trusted Computing Base) mà mọi chứng minh của Lean đều dựa vào.

Hàm này có nhiệm vụ cấp phát bộ nhớ cho các mảng trong Lean. Vấn đề xảy ra khi kích thước cấp phát (capacity) gần bằng SIZE_MAX (giá trị tối đa của kiểu số nguyên 64-bit). Phép cộng sizeof(lean_sarray_object) + elem_size * capacity bị tràn (wrap around), dẫn đến việc runtime chỉ cấp phát một vùng nhớ rất nhỏ (khoảng 23 byte), trong khi chương trình vẫn cố gắng ghi một lượng dữ liệu khổng lồ vào đó.

Một tệp ZIP chỉ 156 byte với trường compressedSize được thiết kế đặc biệt là đủ để kích hoạt lỗi này và gây ra tràn bộ nhớ heap.

Tại sao kiểm chứng hình thức bỏ lỡ các lỗi này?

Đối với lỗi từ chối dịch vụ (DoS), lý do khá đơn giản: trình phân tích cú pháp lưu trữ (archive parser) chưa bao giờ được kiểm chứng. Các chứng minh của lean-zip chỉ bao gồm quy trình nén và giải nén (DEFLATE, Huffman, CRC32), trong khi module đọc header ZIP không có bất kỳ định lý (theorem) nào bảo vệ nó. Dữ liệu từ header không tin cậy được truyền thẳng vào hàm cấp phát mà không qua bước xác thực.

Đối với lỗi tràn bộ nhớ trong runtime, vấn đề sâu sắc hơn. Runtime được viết bằng C++ và được giả định là đúng đắn. Một lỗi ở tầng nền tảng này không chỉ ảnh hưởng đến lean-zip mà còn ảnh hưởng đến mọi chương trình Lean 4 khác sử dụng ByteArray.

Leo De Moura và triết lý kiểm chứng

Kết luận

Kết quả tích cực ở đây là đáng kể. Qua 105 triệu lần thực thi, mã ứng dụng (loại trừ runtime) không có lỗi tràn heap, không có use-after-free, và không có hành vi undefined. Hệ thống kiểu của Lean với các kiểu phụ thuộc đã loại bỏ hoàn toàn các lớp lỗi thường thấy trong các bản cài đặt C/C++.

Tuy nhiên, hai lỗi được tìm thấy đều nằm ngoài ranh giới của các chứng minh. Một lỗi là do thiếu đặc tả kỹ thuật (specification), và lỗi kia là do vấn đề trong chính nền tảng mà chúng ta tin tưởng. Kiểm chứng hình thức chỉ mạnh mẽ bằng những câu hỏi bạn nghĩ ra và những nền tảng bạn chọn để tin tưởng.

Như người La Mã đã nói: Quis custodiet ipsos custodes? (Ai sẽ canh gác những người canh gác?).