Nhân hệ điều hành Linux, một trong những nền tảng được kiểm thử nghiêm ngặt bậc nhất thế giới chạy trên hàng tỷ thiết bị, vừa ghi nhận hơn 1.000 lỗ hổng bảo mật được công bố. Các biện pháp phòng thủ an ninh mạng truyền thống dần trở nên quá tải khi các mô hình trí tuệ nhân tạo thế hệ mới có thể xâu chuỗi các lỗi nhỏ lẻ thành chuỗi khai thác bảo mật nghiêm trọng. Thực tế này đòi hỏi một phương pháp luận khác biệt: chứng minh toán học rằng phần mềm hoàn toàn không chứa lỗi.
Đột phá kiểm chứng mã nguồn ở cấp độ hợp ngữ
Phương pháp kiểm chứng hình thức (formal verification) chuyển đổi mã nguồn thành các mô hình toán học nhằm chứng minh chương trình luôn tuân thủ bộ quy tắc an ninh nghiêm ngặt. Dù mang lại độ tin cậy tuyệt đối, quy trình này từng đòi hỏi chi phí và thời gian khổng lồ. Điển hình như việc phát triển hệ điều hành seL4 chỉ mất 2 năm-người (person-years), nhưng nhóm nghiên cứu đã phải tiêu tốn tới 20 năm-người để hoàn tất việc kiểm chứng hình thức.
Hợp tác cùng đơn vị nghiên cứu Theorem, nhóm chuyên gia tại Anthropic gồm Keane Lucas, Aengus Lynch, Nickolai Zeldovich cùng các cộng sự đã chứng minh các mô hình ngôn ngữ lớn (LLMs) có thể đảo ngược thực trạng trên. Nhóm nghiên cứu đã ứng dụng mô hình Claude để thiết lập các chứng minh bảo mật tự động ở cấp độ mã hợp ngữ (assembly code) dựa trên kiến trúc RISC-V trên hơn 100 thư viện phần mềm mã nguồn mở thực tế.
Tự động hóa xây dựng đặc tả kỹ thuật
Thử nghiệm được triển khai trên 123 thư viện mã nguồn mở. Claude đã chứng minh thành công việc các tệp thực thi này sẽ không bao giờ gặp lỗi sập chương trình dưới các điều kiện quy định: chương trình luôn thoát bình thường, không kích hoạt lỗi an toàn bộ nhớ (memory safety) hay vi phạm câu lệnh kiểm định (assertions) với mọi đầu vào dưới 64 MB.
Rào cản lớn nhất của kiểm chứng quy mô lớn nằm ở đặc tả kỹ thuật (specification). Để giải quyết bài toán định nghĩa một phần mềm hoạt động ‘đúng’, nhóm nghiên cứu đã tự động hóa việc chuyển đổi các bộ kiểm thử sẵn có (test suites) thành đặc tả toán học với nguyên lý ‘bộ kiểm thử này luôn phải vượt qua’. Khả năng duyệt và xử lý hàng triệu dòng mã của mô hình ngôn ngữ lớn đã giúp việc tạo lập các chứng chỉ toán học phức tạp cho hàng chục nghìn chỉ lệnh hợp ngữ trở nên khả thi về mặt kỹ thuật.
Khám phá lỗ hổng tồn tại nhiều năm
Đáng chú ý, trong quá trình lập luận và chứng minh toán học, Claude đã phát hiện ra các lỗ hổng bảo mật đã tồn tại nhiều năm trong mã nguồn mở, vốn không bị phát hiện dù đã trải qua hàng nghìn tỷ lượt kiểm thử tự động (fuzzing). Anthropic và Theorem cũng đang mở rộng phương pháp này nhằm đánh giá độ an toàn của thuật toán nén zlib và kiểm chứng tính tương đương hành vi của trình thông dịch Python viết bằng ngôn ngữ Rust.
Nhóm nghiên cứu đang công bố công khai tập hợp các chứng minh này cùng ngữ nghĩa vận hành của RISC-V trên hệ điều hành Linux để cộng đồng lập trình viên có thể kiểm chứng độc lập và ứng dụng vào các chu trình phát triển phần mềm an toàn trong tương lai.
Nguồn: Anthropic
Liên hệ qua Zalo
