oss-fuzz

Công ty trí tuệ nhân tạo Anthropic đã phát hành nghiên cứu từ nhóm Frontier Red Team vào ngày 22 tháng 10, cho biết các mô hình ngôn ngữ lớn đã có thể tự động viết chứng minh hình thức ở quy mô lớn hơn. Nhóm đã hợp tác với Theorem, sử dụng Claude ở cấp độ lắp ráp RISC-V để chứng minh các thuộc tính an toàn của hơn 100 thư viện mã nguồn mở thực tế, và cho biết đây là lần đầu tiên được biết đến việc sử dụng AI để thực hiện xác minh hình thức quy mô lớn cho phần mềm sản xuất ở cấp độ lắp ráp. Trong quá trình viết chứng minh, nhóm cũng phát hiện ra những lỗ hổng chưa được phát hiện trong nhiều năm.Thí nghiệm đã chuyển đổi các bài kiểm tra fuzz có thể biên dịch đã có trong Google OSS-Fuzz thành các đặc tả: dưới các giả định về nhị phân tĩnh đơn luồng, ngân sách bộ nhớ cố định, CPU RISC-V và Linux, đối với bất kỳ đầu vào nào nhỏ hơn 64 MB, chương trình phải thoát bình thường và không kích hoạt lỗi an toàn bộ nhớ hoặc thất bại xác nhận. Trong vài tuần, Claude đã chứng minh các thuộc tính trên cho 239 điểm vào trong 123 thư viện OSS-Fuzz sau khi sửa chữa các vấn đề đã phát hiện. Chứng minh nhắm vào các lệnh RISC-V đã biên dịch, khoảng 180 triệu dòng Rocq, và được kiểm tra bởi nhân Rocq. Trang web cho biết, điều này không có nghĩa là các thư viện này không có lỗ hổng, các vấn đề còn lại có thể nằm ngoài các thành phần đáng tin cậy hoặc phạm vi chứng minh.Trang web cũng cho biết, nhóm đã yêu cầu Claude hình thức hóa RFC 1950 và chứng minh rằng việc triển khai zlib trong nhân Linux tuân thủ đặc tả đó ở cấp độ nhị phân x86; một trình thông dịch viết bằng Rust bao phủ một tập con lớn của Python, tỷ lệ nhất quán với hành vi của CPython cho hơn 1.7 triệu chương trình được tạo ngẫu nhiên là 99.95%. Trong 36 nhiệm vụ xác minh nhỏ, Opus 5.5 đã chứng minh rằng một nửa số token cần thiết ít hơn khoảng 40% so với Opus 5. Nhóm cũng chỉ ra rằng, chứng minh nhắm vào nhị phân RISC-V liên kết tĩnh đơn luồng, và bộ kiểm tra chứng minh không thể xác định xem đặc tả có phù hợp với thực tế hay không.