Anthropic đã trình bày kết quả các thí nghiệm sử dụng mô hình AI để xác minh chính thức độ tin cậy và bảo mật của các dự án hiện có. Trong thí nghiệm, các mô hình AI đã được sử dụng để tạo ra các bằng chứng toán học về việc không có lỗi bộ nhớ đối với 123 thư viện mã nguồn mở được kiểm thử trong cơ sở hạ tầng OSS Fuzz.
Quá trình xác minh được thực hiện ở cấp độ mã hợp ngữ đã biên dịch cho kiến trúc RISC-V. Tổng khối lượng bằng chứng được tạo ra lên tới khoảng 180 triệu dòng mã cho hệ thống xác minh Rocq Prover (khoảng 600 dòng mỗi tệp nhị phân với 18 lệnh RISC-V). Các bằng chứng được tạo ra bằng cách tự động chuyển đổi các bài kiểm tra fuzzing hiện có thành các đặc tả chính thức, sau đó mô hình AI Claude chứng minh rằng chương trình không có lỗi đối với bất kỳ dữ liệu đầu vào nào lên đến 64 MB.
Trong quá trình xây dựng bằng chứng, mô hình AI đã có thể xác định và chuẩn bị các bản vá lỗi cho hàng trăm lỗi trước đây chưa được phát hiện bằng phương pháp kiểm thử mờ (fuzz testing). Trong số đó, có các lỗ hổng tràn bộ đệm khi xử lý một số dữ liệu đầu vào nhất định (ví dụ: CVE-2026-56132 trong libexpat), cũng như các lỗi logic. Hơn nữa, mô hình AI đã được sử dụng để chứng minh sự phù hợp của việc triển khai thuật toán zlib trong nhân hệ điều hành. Linux Thông số kỹ thuật RFC 1950.
Một trình thông dịch cho một tập hợp con của Python cũng được tạo ra bằng Rust, và bằng chứng chính thức về sự phù hợp với ngữ nghĩa của CPython đã được chuẩn bị bằng cách sử dụng bộ công cụ Verus. Để so sánh hành vi với CPython, hơn 1.7 triệu chương trình Python được tạo ngẫu nhiên đã được thực thi. Trong 99.95% trường hợp, kết quả thực thi các chương trình này trong phiên bản mới và trong CPython trùng khớp, và bất kỳ sự khác biệt nào được tìm thấy đều là các trường hợp ngoại lệ đã biết.
Xác minh hình thức đảm bảo tuân thủ đặc tả, nhưng nó không loại bỏ hoàn toàn các vấn đề bảo mật, vì các rủi ro do vấn đề đa luồng, liên kết động và hành vi bất thường trên phần cứng thực tế vẫn chưa được chính thức hóa. Một lợi thế quan trọng của phương pháp đề xuất là nó hoạt động trực tiếp với các tệp nhị phân, loại bỏ nhu cầu viết lại mã hiện có bằng các ngôn ngữ có thể xác minh hình thức.
Nguồn: opennet.ru
