Anthropic cho biết Claude đã chứng minh các thuộc tính bảo mật trên 123 thư viện

Ngày 22 tháng 10 năm 2026, Anthropic công bố nghiên cứu cho biết Claude đã tạo ra các chứng minh hình thức được kiểm tra bằng máy về những thuộc tính bảo mật ở cấp mã hợp ngữ RISC-V, áp dụng cho 239 điểm đầu vào của các bài kiểm thử fuzz trên 123 thư viện mã nguồn mở, trong một dự án hợp tác với Theorem.

Theo Anthropic, Claude đã vá các lỗi tìm được, sau đó chứng minh rằng chương trình sẽ luôn kết thúc bình thường mà không phát sinh lỗi an toàn bộ nhớ hay làm thất bại các xác nhận, với mọi đầu vào nhỏ hơn 64 MB, mọi phản hồi của hệ điều hành Linux được mô hình hóa và mọi bố cục bộ nhớ. Các chứng minh giả định chương trình chạy dưới dạng tệp nhị phân tĩnh, đơn luồng, với ngân sách bộ nhớ cố định trên CPU RISC-V sử dụng Linux. Anthropic cho biết các chứng minh gồm khoảng 180 triệu dòng Rocq; một chứng minh điển hình dài khoảng 600.000 dòng để bao quát các tệp nhị phân có độ dài trung vị là 18.000 lệnh RISC-V. Công ty cho biết, theo hiểu biết của mình, đây là nỗ lực quy mô lớn đầu tiên sử dụng AI để áp dụng phương pháp kiểm chứng hình thức cho phần mềm sản xuất ở cấp mã hợp ngữ.

Một phần các chứng minh, cùng với ngữ nghĩa của RISC-V và hệ điều hành làm cơ sở cho chúng, đang được công bố trên GitHub. Anthropic cho biết họ cũng phát hành các thành phần đáng tin cậy được xây dựng cho dự án nhưng chưa được công khai, các chứng minh hoàn chỉnh cho những bài kiểm thử fuzz không cần vá, cùng các đặc tả cho những bài kiểm thử fuzz mà họ không thể chứng minh; đồng thời, công ty không công bố các chứng minh có thể làm lộ một lỗi chưa được vá.

Chuyển bài kiểm thử fuzz thành chứng minh hình thức

Phương pháp này chuyển bài kiểm thử fuzz hiện có, có thể biên dịch, của mỗi thư viện thành một đặc tả hình thức thể hiện một quy tắc: bài kiểm thử không bao giờ bị treo với bất kỳ đầu vào nào nhỏ hơn 64 MB. Đặc tả được định nghĩa trên các lệnh RISC-V đã biên dịch, sử dụng ngữ nghĩa hình thức của tập lệnh RISC-V và các tiến trình Linux do Theorem xây dựng; bộ kiểm tra chứng minh Rocq xác minh từng chứng minh hoàn tất theo đặc tả đó. Anthropic cho biết cách làm này chỉ còn lại ba thành phần mà nhà phát triển cần tin cậy: các mô hình hình thức của RISC-V và tiến trình Linux, các phát biểu định lý chính xác và bản thân bộ kiểm tra Rocq.

Anthropic cho biết họ đã áp dụng quy trình này cho hàng trăm dự án trong sáng kiến OSS-Fuzz của Google, nơi cung cấp kiểm thử fuzz liên tục cho các dự án mã nguồn mở đủ điều kiện và tự động gắn công cụ đo lường vào các chương trình C và C++ bằng AddressSanitizer, một công cụ làm chương trình bị treo mỗi khi truy cập bộ nhớ không đúng cách. Phụ lục đề ngày 22 tháng 10 năm 2026 nêu đầy đủ định lý được chứng minh: với mọi đầu vào nhỏ hơn 64 MiB và mọi bố cục bộ nhớ, cả tệp nhị phân được gắn AddressSanitizer lẫn tệp nhị phân thông thường đều không gặp lỗi, không bị hủy bỏ và không biểu hiện hành vi ngoài mô hình; đồng thời, cả hai tạo ra các dấu vết đọc và ghi, hành vi kết thúc và trạng thái hệ thống tệp cuối cùng giống hệt nhau.

Phụ lục cho biết Claude đã viết khoảng một tỷ dòng Rocq trong quá trình thực hiện, trong đó khoảng 180 triệu dòng vượt qua bộ kiểm tra chứng minh; điểm vào của trình phân tích cú pháp 391 dòng trong cJSON nhận được một chứng minh dài 630.000 dòng, còn fftw3, với 51.000 dòng được liên kết vào, nhận được một chứng minh dài 480.000 dòng. Vì Claude được phép vá mã trước khi hoàn tất chứng minh, Anthropic cho biết họ đã phạt các bản vá, thưởng thêm điểm nếu chứng minh được bản vá làm thay đổi đầu vào nào, đồng thời ghi lại và kiểm tra các bản vá để ngăn việc thao túng phần thưởng.

Lỗi được phát hiện trong quá trình thử chứng minh

Anthropic cho biết quá trình thử chứng minh đã làm lộ ra hàng trăm lỗi, trong đó có nhiều lỗi mà công cụ fuzz khó có thể phát hiện. Khi chứng minh điểm vào của một thư viện, Claude phát hiện lỗi tràn xuống của bộ đếm trong một chương trình giải nén, gây ra thao tác ghi vượt phạm vi, nhưng chỉ với các đầu vào có dung lượng khoảng 20 MB và một bố cục hiếm gặp, cụ thể. Những phát hiện khác gồm lỗi đọc vượt phạm vi trong bộ giải mã hình ảnh, cần đầu vào 64 MB và hơn 2 GB bộ nhớ; lỗi đọc vượt phạm vi đòi hỏi một chuỗi lệnh gọi cụ thể qua hai tay cầm cùng trỏ đến một tệp; và việc phát hiện lại CVE-2026-56132 trong libexpat, vốn đòi hỏi đầu vào lồng nhau sâu.

Claude cũng phát hiện các lỗi logic không bao giờ làm chương trình bị treo, trong đó có trường hợp quy định giới hạn những tệp mà ứng dụng có thể tải nhưng giới hạn này không phải lúc nào cũng được thực thi. Anthropic cho biết các nỗ lực kiểm chứng một số ứng dụng trọng yếu được sử dụng rộng rãi đã phát hiện một lỗi logic chưa từng được biết đến, âm ỉ tồn tại hơn một thập kỷ; trong quá trình kiểm chứng một trình đọc PDF được sử dụng rộng rãi, họ đã tìm thấy trong một tuần số lỗi bảo mật bằng với số lỗi thường được báo cáo trong một năm.

Các thử nghiệm bổ sung và phát hiện về hiệu quả

Ngoài OSS-Fuzz, Anthropic yêu cầu Claude viết đặc tả hình thức cho RFC 1950, tài liệu kỹ thuật định nghĩa định dạng nén zlib, rồi chứng minh rằng cách triển khai zlib trong nhân Linux tuân thủ chính xác đặc tả đó. Claude trực tiếp chứng minh tệp nhị phân được biên dịch cho x86, sử dụng ngữ nghĩa hình thức của tập lệnh x86 do Claude tạo ra; Anthropic cho biết họ đã lặp lại quy trình này với nửa tá thư viện được sử dụng rộng rãi khác và phát hiện các lỗi nhỏ, không thể khai thác trong những trường hợp biên, hiện đang được gửi báo cáo cho các dự án liên quan. Công ty cũng cho biết việc tạo ngữ nghĩa x86 đã phát hiện hàng trăm sai sót trong tài liệu tham khảo chính thức và một số ít lỗi trong chính phần cứng; đồng thời, việc thực thi từng bước theo ngữ nghĩa này có thể khởi động môi trường người dùng Ubuntu trên một nhân Linux.

Trong một thử nghiệm khác, Claude đã xây dựng bằng Rust một trình thông dịch hỗ trợ một tập hợp lớn các tính năng của Python, rồi dùng công cụ kiểm chứng Verus để chứng minh rằng trình thông dịch tuân thủ các ngữ nghĩa của CPython được nêu trong một bài báo học thuật. Phụ lục kỹ thuật cho biết cả 17 tầng của trình thông dịch đều đã được chứng minh, với định lý rằng: “Bất cứ khi nào trình thông dịch trả về một kết quả, kết quả đó chính là kết quả mà ngữ nghĩa hình thức quy định.” Anthropic cho biết thử nghiệm thực nghiệm trên 1,7 triệu chương trình Python được tạo ngẫu nhiên cho thấy hành vi của trình thông dịch trùng khớp với CPython trong 99,95% số lần thử; trong số bảy lỗi được cố ý cài vào, năm lỗi vẫn không bị phát hiện qua thử nghiệm ngẫu nhiên, trong khi cả bảy lỗi đều khiến chứng minh không còn đúng.

Để đo lường hiệu quả, Anthropic tạo 36 tác vụ kiểm chứng nhỏ bằng cách thu gọn các điểm đầu vào thực tế của OSS-Fuzz, tạo ra những chương trình gồm 283–2.491 lệnh với đầu vào giới hạn ở 64 byte, đồng thời thay AddressSanitizer bằng một môi trường chạy “mini-ASan” khoảng 100 lệnh. Anthropic cho biết Opus 5.5 chứng minh được một nửa số tác vụ với lượng token ít hơn khoảng 40% so với Opus 5. Anthropic cũng cho biết các tác nhân được phép sao chép chứng minh của nhau trong một không gian làm việc chung cần ít hơn 17% token so với các tác nhân làm việc riêng lẻ; một số tác nhân thành công sau khi trước đó thất bại khi làm một mình, còn các tác nhân làm việc riêng lẻ không hoàn thành được hai chứng minh. Công ty cho biết hiệu ứng tái sử dụng tương tự cũng xuất hiện ở quy mô lớn trong nỗ lực OSS-Fuzz, khi các nhóm tác nhân sao chép những chứng minh đã hoàn tất rồi điều chỉnh chúng, bởi phần lớn nội dung của mỗi chứng minh liên quan đến mã khởi tạo dùng chung của môi trường chạy C và AddressSanitizer.

Những hạn chế được nêu và chương trình OSS Verify

Anthropic cho biết các chứng minh không có nghĩa là những thư viện này không còn lỗi: các lỗi còn sót lại có thể nằm trong những thành phần được tin cậy hoặc ngoài phạm vi của các chứng minh. Các chứng minh áp dụng cho các tệp nhị phân RISC-V tĩnh, đơn luồng, được liên kết với musl libc, trong khi phần lớn người dùng chạy những thư viện này trên x86 hoặc ARM và liên kết động với glibc; ngoài ra, AddressSanitizer không phát hiện được tất cả các lỗi an toàn bộ nhớ. Công ty cho biết họ kỳ vọng những hạn chế này sẽ trở nên có thể xử lý khi các mô hình được cải thiện.

Theorem cung cấp miễn phí quy trình tương tự cho các dự án mã nguồn mở đủ điều kiện thông qua chương trình OSS Verify. Các dự án đăng ký bằng cách gửi yêu cầu kéo bổ sung các tệp project.yaml, Dockerfile và build.sh vào kho lưu trữ của chương trình; Theorem cho biết họ đánh giá các dự án theo những tiêu chí tương tự OSS-Fuzz, ưu tiên hạ tầng thiết yếu được sử dụng rộng rãi. Theo Theorem, những người duy trì dự án sẽ nhận được một chứng minh Rocq, được hạt nhân Rocq kiểm tra, cho thấy mỗi mục tiêu fuzz không bị lỗi khi gặp bất kỳ đầu vào nào có kích thước tối đa 64 MiB; các lỗi phát hiện được trong quá trình chứng minh sẽ được thông báo riêng cho người duy trì qua email, không có thời hạn công bố, và việc tạo ra chứng minh có thể mất nhiều ngày. Lộ trình của Theorem đặt mục tiêu kiểm chứng toàn bộ hệ sinh thái Nix, bao gồm các hạ tầng thiết yếu như glibc, OpenSSL và cURL.