Google DeepMind trình làng AlphaProof Code, xác minh lõi mã hóa của Signal chỉ trong 4 tuần

Google DeepMind vừa chính thức ra mắt AlphaProof Code, một hệ thống trí tuệ nhân tạo được thiết kế để xác minh bằng toán học rằng phần mềm đáp ứng chính xác các đặc tả kỹ thuật về an toàn mà không xảy ra lỗi.

Trong một cuộc thử nghiệm quy mô lớn nhằm chứng minh năng lực, các nhà nghiên cứu đã sử dụng công nghệ này để kiểm định giao thức mã hóa của ứng dụng nhắn tin bảo mật Signal. AlphaProof Code đã hoàn thành việc xác minh hình thức (formal verification) mã nguồn mã hóa cốt lõi của Signal chỉ trong bốn tuần — một công việc thông thường phải mất nhiều năm nỗ lực của con người.

Xác minh mã nguồn thực tế ở quy mô lớn

Theo các nhà nghiên cứu Pushmeet Kohli và Swarat Chaudhuri của DeepMind, các nỗ lực xác minh hình thức trước đây thường chỉ dừng lại ở các thiết kế trên lý thuyết. AlphaProof Code đã tiến một bước xa hơn khi xác minh trực tiếp mã nguồn mã hóa thực tế đang chạy trên thiết bị của người dùng.

Hệ thống này dựa trên các tác tử AI (AI agents) được xây dựng trên nền tảng Gemini Carbon của Google. Sau khi các chuyên gia đưa ra các yêu cầu bảo mật hình thức, các tác tử AI đã hỗ trợ lập ra bản đặc tả và tạo ra hơn sáu triệu dòng chứng minh hình thức bằng ngôn ngữ Lean, nhằm chứng minh một cách độc lập rằng phần mềm đã đáp ứng đầy đủ các điều kiện đó.

Trong quá trình thực hiện, AI đã gắn cờ khoảng 1% cơ sở mã (codebase) để con người xem xét lại. Để đánh giá độ tin cậy của hệ thống, các nhà nghiên cứu đã cố tình gài hai lỗi (bugs) vào cơ sở mã để kiểm tra và AlphaProof Code đã phát hiện ra cả hai ngay lập tức.

Mở rộng sang các hạ tầng quan trọng

Thành công trong việc xác minh giao thức của Signal đã khẳng định vai trò ngày càng tăng của AI trong việc bảo vệ các hệ thống kỹ thuật số nhạy cảm. Giám đốc Công nghệ (CTO) của Signal, ông Ehren Kret, nhận định rằng phương pháp xác minh này giúp củng cố niềm tin vào quyền riêng tư dữ liệu trong bối cảnh các mối đe dọa an ninh mạng không ngừng biến đổi.

Hướng tới tương lai, Google DeepMind lên kế hoạch mở rộng phương pháp xác minh hình thức này vượt ra ngoài các ứng dụng nhắn tin, hướng đến các hạ tầng quan trọng trong đời sống thực như thiết bị y tế và lưới điện, thông qua việc sử dụng các hệ thống như CodeMender.