LLM giúp kiểm chứng hình thức phần mềm trở nên khả thi ở quy mô lớn

Anthropic vừa công bố một nghiên cứu hợp tác cùng Theorem, cho thấy các mô hình ngôn ngữ lớn (LLM) có thể tự động viết chứng minh hình thức (formal proof) ở mức mã hợp ngữ cho hàng trăm thư viện mã nguồn mở thực tế. Kết quả này mở ra hướng đi mới để đảm bảo an toàn phần mềm ở quy mô chưa từng có.

Đáng chú ý, trong quá trình chứng minh, Claude còn phát hiện nhiều lỗi đã tồn tại âm thầm nhiều năm mà các bài kiểm thử fuzzing với hàng nghìn tỷ lần chạy vẫn không tìm ra.

Vì sao kiểm chứng hình thức lại quan trọng?

Hầu hết phần mềm đều đầy rẫy lỗi, và AI ngày càng giỏi trong việc tìm ra và khai thác chúng. Ngay cả nhân Linux — một trong những phần mềm được kiểm thử kỹ lưỡng nhất, chạy trên hàng tỷ thiết bị — gần đây cũng ghi nhận hơn 1.000 lỗ hổng được công bố.

Các biện pháp phòng thủ truyền thống như kiểm thử, fuzzing hay phân tích tĩnh không còn đủ. Chúng ta cần cách chứng minh mã nguồn không còn lỗi. Kiểm chứng hình thức chính là phương pháp đó: chuyển mã thành mô hình toán học rồi chứng minh nó luôn tuân thủ một tập quy tắc an toàn.

Trước đây, kiểm chứng hình thức đòi hỏi kỹ năng cực kỳ chuyên biệt. Nhân hệ điều hành seL4 mất 2 năm-người để lập trình nhưng tới 20 năm-người để kiểm chứng hình thức.

Minh họa quy trình kiểm chứng hình thức với LLM

Biến bài kiểm thử thành chứng minh

Nhóm nghiên cứu chọn cách tiếp cận thực dụng: biến các bộ kiểm thử fuzz có sẵn của thư viện thành đặc tả (spec). Cụ thể, họ mã hóa quy tắc "bộ kiểm thử này luôn chạy qua" dựa trên mô hình tổng quát về cách một chương trình biên dịch cho RISC-V chạy trên Linux.

Sau đó Claude viết chứng minh rằng chương trình sẽ không bao giờ gặp sự cố với mọi đầu vào dưới 64 MB. Nếu chứng minh thành công, việc fuzzing điểm vào đó trở nên dư thừa — sẽ không còn lỗi nào để tìm.

Kết quả trong vài tuần:

• 239 điểm vào thuộc 123 thư viện OSS-Fuzz của Google đã được chứng minh không còn sự cố.
• Tổng cộng khoảng 180 triệu dòng chứng minh viết bằng Rocq, mỗi chứng minh điển hình dài khoảng 600.000 dòng cho các tệp nhị phân có độ dài trung vị 18.000 lệnh RISC-V.
• Chứng minh được kiểm tra tự động bởi nhân Rocq, nên gần như không cần con người rà soát thủ công.

Điều đáng chú ý là Claude không chỉ chứng minh mà còn tự sửa lỗi khi gặp trở ngại, rồi chứng minh lại trên mã đã vá. Nhóm nghiên cứu cho biết họ đã ghi log và kiểm toán các bản vá để tránh hiện tượng "reward hacking" — khi mô hình tìm cách lách mục tiêu thay vì thực sự giải quyết vấn đề.

Những lỗi mà fuzzing bỏ lỡ

Nhiều lỗi được phát hiện nằm ngoài tầm với của fuzzing thông thường, vốn chỉ xử lý đầu vào nhỏ (thường dưới 1 MB) và dựa vào độ phủ mã để định hướng.

• Một lỗi tràn số dưới trong bộ giải nén gây ghi ngoài biên, chỉ kích hoạt với đầu vào khoảng 20 MB có bố cục hiếm gặp.
• Một lỗi đọc ngoài biên trong bộ giải mã ảnh cần tới 64 MB đầu vào và hơn 2 GB bộ nhớ.
• Một lỗi trong thư viện khác chỉ xuất hiện khi gọi theo một trình tự cụ thể qua hai handle cùng trỏ tới một tệp.
• Tái phát hiện CVE-2026-56132 trong libexpat, cần đầu vào lồng nhau rất sâu.
• Cả những lỗi logic không gây crash, ví dụ một tính năng giới hạn tệp được phép tải nhưng không phải lúc nào cũng được thực thi.

Quy trình chứng minh bất biến không sự cố

Vượt xa khỏi an toàn bộ nhớ

Việc chứng minh một bài kiểm thử fuzz không còn gây crash có ý nghĩa lớn hơn tên gọi. Nhiều bài kiểm thử thực tế kiểm tra các thuộc tính cấp cao như mã hóa rồi giải mã phải trả về dữ liệu gốc, tính bất biến (idempotence), các luật đại số hay so sánh với bản tham chiếu. Chứng minh bài kiểm thử không crash tương đương với chứng minh chính thuộc tính đó.

Có trường hợp thú vị: để hoàn tất chứng minh cho cpp-httplib, Claude buộc phải chứng minh ở mức mã máy rằng thuật toán cân bằng cây đỏ-đen của libc++ thực sự giữ được độ sâu cây ở mức logarit.

Nhóm nghiên cứu cũng thử nghiệm các hướng khác:

• Viết đặc tả hình thức cho RFC 1950 rồi chứng minh bản zlib trong nhân Linux tuân thủ đúng đặc tả đó, ở mức nhị phân biên dịch cho x86.
• Xây dựng trình thông dịch Python viết bằng Rust và chứng minh nó tuân theo ngữ nghĩa CPython (dùng công cụ Verus), sau đó kiểm tra thực nghiệm trên hơn 1,7 triệu chương trình ngẫu nhiên, đạt độ khớp 99,95%.
• Khi kiểm chứng một trình đọc PDF phổ biến, phát hiện số lỗi bảo mật trong một tuần bằng cả năm báo cáo thông thường.

Bài học về chi phí và khả năng tái sử dụng

Một hạn chế lớn hiện nay là chứng minh có thể tốn hàng trăm triệu token. Tuy vậy, dữ liệu cho thấy chi phí đang giảm nhanh:

• Trên 36 bài kiểm chứng nhỏ lấy từ mã OSS-Fuzz, Opus 5.5 chứng minh được một nửa với lượng token ít hơn khoảng 40% so với Opus 5.
• Khi các agent được chia sẻ không gian làm việc chung để sao chép chứng minh của nhau, chúng cần ít hơn 17% token so với làm việc độc lập, và một số bài trước đó thất bại nay đã thành công.
• Ở quy mô lớn, phần lớn chứng minh liên quan tới mã khởi tạo runtime C và AddressSanitizer mà chương trình nào cũng có, nên các nhóm agent có thể sao chép và tinh chỉnh chứng minh sẵn có cho chương trình mới.

Cách tích lũy này tương tự cách Mathlib — thư viện toán học hình thức dùng Lean — phát triển lên gần 300.000 định lý nhờ hơn 700 người đóng góp, mỗi chứng minh mới đều dựa trên khối tài sản cũ.

Biểu đồ tái sử dụng chứng minh giữa các agent

Giới hạn cần lưu ý

Nhóm tác giả thẳng thắn thừa nhận: "được kiểm chứng hình thức" không đồng nghĩa với "không còn lỗi". Trình kiểm tra chứng minh không thể xác nhận đặc tả có phản ánh đúng thực tế hay không.

Các chứng minh hiện tại giả định chương trình là tệp nhị phân tĩnh, đơn luồng, liên kết với musl libc và chạy trên RISC-V với Linux. Trong khi đó phần lớn người dùng chạy thư viện trên x86 hoặc ARM và liên kết động với glibc. Bên cạnh đó, AddressSanitizer không phát hiện mọi lỗi an toàn bộ nhớ, và việc kiểm chứng các điểm vào không bao phủ toàn bộ thư viện.

Những thành phần cần tin cậy gồm: mô hình hình thức của RISC-V và tiến trình Linux, phát biểu định lý được chứng minh, và bản thân trình kiểm tra Rocq. Thu hẹp và gia cố các khoảng trống này là hướng nghiên cứu tiếp theo.

Ý nghĩa với cộng đồng phát triển phần mềm

Với các lập trình viên và doanh nghiệp Việt Nam, đặc biệt những đơn vị đang xây dựng hệ thống tài chính, thương mại điện tử hay hạ tầng đám mây dựa nhiều trên thư viện mã nguồn mở, hướng tiếp cận này có thể giúp giảm rủi ro bảo mật ở tầng gốc thay vì chỉ vá lỗi bề mặt.

Theorem đang cung cấp dịch vụ chạy quy trình tương tự cho các dự án mã nguồn mở khác, đồng thời công bố một skill cho Claude giúp lập trình viên bắt đầu kiểm chứng mã của mình. Nhóm tác giả cũng kêu gọi cộng đồng tự kiểm tra độc lập các chứng minh đã công bố.

"Kiểm chứng hình thức, từ chỗ chỉ khả thi cho những dòng mã an toàn tối quan trọng như hệ thống điện tử hàng không, sẽ sớm trở nên phổ biến như fuzzing ngày nay."

Khi mà LLM ngày càng tự động quét và tìm ra nhiều lỗ hổng hơn, việc dùng chính LLM để xây dựng bảo đảm an toàn phần mềm ở quy mô lớn là một hướng đi đáng theo dõi trong những năm tới.