LLM tự động hóa quy trình xác minh hình thức cho các thư viện mã nguồn mở ở quy mô lớn

Các nhà phát triển phần mềm từ lâu đã phải vật lộn với chi phí cao của việc xác minh hình thức (formal verification), một phương pháp sử dụng toán học để chứng minh code không chứa các lỗi cụ thể. Một dự án hợp tác gần đây giữa nhóm nghiên cứu AI và Theorem cho thấy các mô hình ngôn ngữ lớn giờ đây có thể tự động hóa quy trình này ở quy mô lớn. Bằng cách sử dụng Claude để phân tích các binary đã biên dịch, nhóm đã thành công trong việc chứng minh các thuộc tính bảo mật cho hơn 100 thư viện mã nguồn mở thực tế, đánh dấu một bước chuyển mình quan trọng trong cách đảm bảo tính đúng đắn của phần mềm.

Chuyện gì đã xảy ra

Dự án tập trung vào việc áp dụng xác minh hình thức cho phần mềm sản xuất ở cấp độ mã assembly, cụ thể là nhắm mục tiêu vào kiến trúc RISC-V. Nhóm đã chọn 123 thư viện mã nguồn mở từ chương trình OSS-Fuzz của Google, vốn đã chứa hàng nghìn điểm nhập (entry points) do lập trình viên viết sẵn, được thiết kế để gây sập khi tìm thấy lỗi. Thay vì dựa vào kiểm thử brute-force, nhóm yêu cầu Claude chứng minh rằng các chương trình này sẽ không bao giờ bị sập với bất kỳ đầu vào nào dưới 64 MB, giả định chạy trên Linux với binary tĩnh đơn luồng.

Trong vài tuần, Claude đã tạo ra các bằng chứng cho 239 điểm nhập xuyên suốt các thư viện này. Tổng cộng, các bằng chứng tạo ra khoảng 180 triệu dòng mã Rocq, với mỗi bằng chứng trung bình dài khoảng 600.000 dòng. Trong quá trình này, mô hình không chỉ tạo ra các bằng chứng mà còn xác định và vá các lỗi vẫn tồn tại mặc dù đã qua hàng nghìn tỷ lần chạy kiểm thử trước đó. Nỗ lực này đại diện cho ứng dụng quy mô lớn đầu tiên của AI vào việc xác minh hình thức phần mềm sản xuất ở cấp độ assembly.

Để làm cho những phát hiện này dễ tiếp cận, nhóm đang công bố một tập con các bằng chứng cùng với ngữ nghĩa của RISC-V và hệ điều hành được sử dụng trong phân tích. Theorem cũng cung cấp dịch vụ chạy pipeline xác minh này cho các dự án mã nguồn mở khác và đã phát hành một kỹ năng (skill) cho Claude để giúp các nhà phát triển bắt đầu xác minh code của chính họ. Cách tiếp cận này đưa xác minh hình thức từ một thực hành ngách dành riêng cho các hệ thống quan trọng như hàng không vũ trụ trở thành một công cụ áp dụng rộng rãi hơn cho phát triển phần mềm nói chung.

Cách hoạt động

Xác minh hình thức đòi hỏi phải chuyển đổi code sang một mô hình toán học và chứng minh nó tuân thủ một bộ quy tắc bảo mật. Thách thức chính luôn là định nghĩa thế nào là "đúng" đối với phần mềm phức tạp. Trong dự án này, nhóm đã bỏ qua nhu cầu về đặc tả thủ công bằng cách chuyển đổi các bài kiểm thử fuzz hiện có thành các đặc tả hình thức. Kiểm thử fuzz tạo ra các đầu vào ngẫu nhiên để tìm lỗi sập, nhưng chúng không thể đảm bảo mọi đường dẫn đều được kiểm tra. Phương pháp mới định nghĩa đặc tả là "bộ kiểm thử này luôn pass", áp dụng cho các lệnh RISC-V đã biên dịch thay vì mã nguồn.

Claude hoạt động bằng cách phân tích các artifact thực thi và ngữ nghĩa hình thức của tập lệnh RISC-V cũng như hành vi tiến trình Linux do Theorem cung cấp. Mô hình tạo ra các bằng chứng khổng lồ chứng minh rằng không có lỗi an toàn bộ nhớ hoặc lỗi assertion nào có thể xảy ra trong các điều kiện đã định nghĩa. Các bằng chứng này sau đó được xác thực bởi trình kiểm tra bằng chứng Rocq, một kernel tin cậy đảm bảo logic toán học là đúng. Vì trình kiểm tra tự động xác thực bằng chứng, các nhà phát triển không cần phải xem xét thủ công hàng triệu dòng code được tạo ra, mà chỉ cần tin tưởng vào các mô hình cơ bản và chính trình kiểm tra.

Chi tiết chính

• Dự án đã xác minh 239 điểm nhập xuyên suốt 123 thư viện mã nguồn mở từ chương trình OSS-Fuzz.
• Claude tạo ra khoảng 180 triệu dòng mã bằng chứng Rocq, với các bằng chứng điển hình đạt tới 600.000 dòng.
• Việc xác minh nhắm mục tiêu vào mã assembly RISC-V, chứng minh không có lỗi sập cho các đầu vào dưới 64 MB trên Linux.
• Mô hình đã phát hiện và vá các lỗi sống sót qua hàng nghìn tỷ lần chạy kiểm thử fuzz trước đó.
• Niềm tin được đặt vào các mô hình hình thức của RISC-V và Linux, các tuyên bố định lý và trình kiểm tra bằng chứng Rocq.
• Theorem đang phát hành một kỹ năng cho Claude để hỗ trợ các nhà phát triển áp dụng các quy trình xác minh tương tự cho dự án của riêng họ.

Tại sao điều này quan trọng

Đối với các kỹ sư phần mềm, sự phát triển này hạ thấp rào cản gia nhập cho xác minh hình thức, vốn trước đây đòi hỏi nhiều năm nỗ lực chuyên môn của các chuyên gia. Bằng cách tự động hóa việc tạo ra các bằng chứng, LLM giúp khả thi hóa việc áp dụng các đảm bảo bảo mật nghiêm ngặt cho các thư viện và ứng dụng hàng ngày. Sự chuyển dịch này cho phép các đội ngũ vượt ra khỏi việc sửa lỗi phản ứng và kiểm thử fuzz chủ động, hướng tới một mô hình nơi các thành phần quan trọng được chứng minh bằng toán học là an toàn khỏi cả một lớp lỗ hổng, chẳng hạn như lỗi an toàn bộ nhớ.

Khả năng xác minh các binary đã biên dịch thay vì chỉ mã nguồn là đặc biệt quan trọng. Điều này có nghĩa là các thuộc tính bảo mật có thể được đảm bảo cho các artifact thực tế được triển khai trong môi trường production, tính đến cả hành vi của compiler và các tương tác cấp thấp. Khi khả năng của mô hình cải thiện và ngữ nghĩa cho nhiều kiến trúc hơn trở nên khả dụng, cách tiếp cận này có thể trở thành một phần tiêu chuẩn của vòng đời phát triển phần mềm, giảm rủi ro khai thác trong các dependency mã nguồn mở được sử dụng rộng rãi.

Bạn có thể làm gì

• Khám phá tập con các bằng chứng và ngữ nghĩa RISC-V đã công bố để hiểu cấu trúc của xác minh hình thức do AI tạo ra.
• Thử nghiệm kỹ năng Claude mới do Theorem phát hành để bắt đầu thử nghiệm các quy trình xác minh trên codebase của bạn.
• Xem xét lại các bài kiểm thử fuzz hiện có trong dự án của bạn, vì chúng có thể đóng vai trò là nền tảng cho các đặc tả hình thức trong các nỗ lực xác minh tương lai.
• Cân nhắc tích hợp các bước xác minh hình thức cho các thư viện quan trọng trong chuỗi dependency của bạn, đặc biệt là những thư viện xử lý đầu vào không đáng tin cậy.
• Cập nhật thường xuyên các diễn biến về ngữ nghĩa hình thức của RISC-V và Linux, vì việc mở rộng các mô hình này sẽ tăng phạm vi phần mềm có thể xác minh được.
• Đánh giá xem các giả định về binary tĩnh đơn luồng có áp dụng cho các dự án hiện tại của bạn hay không, như một điểm khởi đầu cho việc xác minh.