DeepMind dùng AI chứng minh bảo mật của Signal

Các nhà nghiên cứu của Google DeepMind vừa hoàn tất kiểm chứng hình thức (formal verification) đối với cơ chế bảo mật của Signal. Theo nhóm nghiên cứu, đây là lần đầu tiên AI hỗ trợ xây dựng một chứng minh liên kết các đảm bảo bảo mật ở cấp giao thức với một triển khai mật mã đang được dùng rộng rãi.

Công việc này được thực hiện bằng AlphaProof Code, một khung đa tác nhân (multi-agent framework) dành cho đặc tả và kiểm chứng phần mềm. Kết quả có ý nghĩa lớn vì kiểm chứng hình thức từ trước đến nay vốn rất tốn kém nhân lực.

Kiểm chứng cái gì và bằng cách nào

AlphaProof Code dựa trên một tác nhân do con người dẫn dắt: tác nhân này viết đặc tả bằng Lean — ngôn ngữ lập trình và trợ lý chứng minh định lý — đánh giá ngữ nghĩa của mã máy, rồi tạo ra chứng minh để Lean kernel đối chiếu với đặc tả.

Trong trường hợp này, AlphaProof Code đã kiểm chứng bắt tay hậu lượng tử PQXDH và Triple Ratchet của Signal, qua đó xác thực thiết kế của libsignal về các thuộc tính:

• Bí mật chuyển tiếp (forward secrecy)
• Xác thực (authentication)
• Bảo mật sau khi bị xâm phạm (post-compromise security)
• Bí mật của bắt tay (handshake secrecy)

Nhóm thực hiện gồm Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton và Pushmeet Kohli. Đây là một bước tiến hướng tới thách thức mà Beneficial AI Foundation đưa ra hồi tháng 4/2026: kiểm chứng hình thức giao thức Signal và ứng dụng Signal bằng Lean.

Quy trình diễn ra qua nhiều bước. Các mô hình khác nhau được dùng để chuyển mục tiêu bảo mật của Signal thành đặc tả toán học do con người rà soát. Dựa trên đặc tả đó, các tác nhân Gemini Carbon được giao viết mã Lean chứng minh tính đúng đắn của triển khai libsignal. Sau khi các tác nhân tạo ra 6,5 triệu dòng mã Lean, nhóm thực hiện một lượt kiểm toán và đánh dấu những phần cần con người xem xét.

Ý nghĩa và giới hạn

Kết quả mang tính lý thuyết: nó giả định mật mã hoàn hảo và không bảo đảm tính bí mật tính toán của từng byte. Dù vậy, đây vẫn là một khẳng định có ý nghĩa về tính đúng đắn của hệ thống.

"Đó là một hệ thống được xây dựng căn bản cho sự hợp tác giữa con người và AI", Swarat Chaudhuri, nhà khoa học nghiên cứu tại Google DeepMind và giáo sư Đại học Texas tại Austin, nói.

Theo Chaudhuri, thông thường người ta bắt đầu chứng minh định lý từ những bài toán đã được nhà toán học hình thức hóa rõ ràng rồi giao cho tác nhân AI. Ở trường hợp này, nhóm nghiên cứu phải tự xác định cần chứng minh điều gì.

"Trong lĩnh vực phương pháp hình thức, chúng tôi luôn tin rằng kiểm chứng là phần khó. Đã có ba, bốn mươi năm nghiên cứu về cách mở rộng quy mô kiểm chứng. Giờ chúng tôi làm được điều đó. Vậy câu hỏi tiếp theo là ta đang kiểm chứng cái gì?", ông nói.

Trong bài báo nghiên cứu "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level", nhóm tác giả lưu ý kiểm chứng hình thức trước đây đòi hỏi nỗ lực phi thường: kiểm chứng hình thức vi nhân seL4 mất 20 người-năm, còn phát triển trình biên dịch C đã kiểm chứng CompCert mất sáu năm.

Nhóm tin AlphaProof Code có thể cắt giảm mạnh chi phí kiểm chứng hình thức, dù công việc với Signal vẫn mất bốn tuần với nhóm năm người và "khá nhiều token".

"Giấc mơ chắc chắn là mở rộng quy mô việc này. Năng lực tấn công của AI đang gia tăng, có rất nhiều hệ thống không an toàn trên khắp thế giới và chúng sẽ bị khai thác", Chaudhuri nói.

Ông cho rằng điều cần làm là áp dụng công nghệ này cho mã nguồn nói chung trên toàn cầu, xác định rõ cần phòng ngừa điều gì và viết các thuộc tính đó ra sao. Nhắc tới dự án liên quan AlphaProof Nexus tập trung vào toán học, ông cho biết bước tiếp theo là áp dụng công nghệ này ngay trong quá trình thiết kế phần mềm, không chỉ với giao thức mật mã mà với mã nói chung.

"Chúng tôi thực sự tin rằng biên giới tiếp theo trong hướng nghiên cứu này không phải là chứng minh mà là đặc tả", ông nói.

Góc nhìn

Với lập trình viên và đội kỹ thuật tại Việt Nam, tín hiệu đáng chú ý không nằm ở việc AI "chứng minh được Signal an toàn", mà ở chỗ chi phí kiểm chứng hình thức có thể giảm xuống mức một nhóm nhỏ cũng thử được. Các dự án hạ tầng, ví điện tử hay hệ thống xử lý thanh toán trong nước thường dựa vào kiểm thử và review thủ công; nếu công cụ kiểu này trưởng thành, những thành phần nhạy cảm như luồng xác thực hay mã hóa có thể được đặc tả và kiểm chứng chặt hơn.

Điểm cần lưu ý là phần khó đang chuyển từ chứng minh sang đặc tả: việc xác định chính xác thuộc tính bảo mật cần bảo đảm vẫn cần con người có chuyên môn. Kết quả của DeepMind cũng giả định mật mã hoàn hảo, nên kiểm chứng hình thức là lớp bổ sung chứ không thay thế kiểm thử, đánh giá lỗ hổng và các biện pháp bảo mật vận hành.