Tóm tắt nhanh
- Ngày 10/11/2026, Google DeepMind công bố hệ thống nhiều AI agent AlphaProof Code đã chứng minh bằng toán học rằng mã triển khai giao thức Signal đáp ứng các đặc tả bảo mật do chuyên gia đề ra.
- Các agent chạy bằng Gemini Carbon viết hơn 6 triệu dòng chứng minh Lean; toàn bộ quá trình mất 4 tuần với đội 5 người, và chỉ khoảng 1% cơ sở mã cần con người xem lại.
- Phạm vi là giao thức cốt lõi (bắt tay PQXDH kháng lượng tử và Triple Ratchet) ở mức mã máy, không phải toàn bộ ứng dụng Signal, và không tìm ra lỗ hổng mới.
- Signal, Google Messages và WhatsApp cùng dựa trên giao thức này, nhưng công bố của DeepMind chỉ nói tới mã libsignal.
Google DeepMind vừa cho biết nhóm nghiên cứu của hãng đã dùng AlphaProof Code, một khung làm việc kết hợp chuyên gia con người với nhiều AI agent, để chứng minh các tính chất bảo mật chính của chính đoạn mã đang chạy bên dưới giao thức Signal, thứ bảo vệ tin nhắn của hàng tỷ cuộc trò chuyện trên Signal và Google Messages. DeepMind nhấn mạnh đây là lần đầu AI được dùng để kiểm minh hình thức một giao thức mật mã phổ biến ở độ sâu này, và cũng là lần đầu phần triển khai của một giao thức như vậy được kiểm minh hình thức bằng bất kỳ phương pháp nào.
Lỗi thật hay nằm ở khoảng hở giữa bản thiết kế và mã chạy trên máy
Kiểm minh hình thức nghĩa là chứng minh bằng toán học rằng một đoạn mã luôn chạy đúng với đặc tả, thay vì chỉ thử nhiều trường hợp rồi hy vọng không sót. Kiểm thử thông thường có thể tìm ra lỗi, nhưng không bao giờ bảo đảm rằng không còn lỗi khác. Với giao thức mật mã, giới nghiên cứu đã phân tích hình thức suốt nhiều thập kỷ, nhưng phần lớn dừng ở mức thiết kế: bản vẽ trên giấy đúng, còn đoạn mã biên dịch ra chạy trên điện thoại có đúng bản vẽ hay không thì ít khi được chứng minh. Lỗ hổng thực tế lại hay nằm đúng ở khoảng hở đó.
Điểm khác của công trình này là các agent chứng minh ở mức mã máy, tức đoạn mã thật sự chạy trên thiết bị. Phần được kiểm minh gồm bắt tay PQXDH kháng lượng tử và cơ chế xoay khóa Triple Ratchet của libsignal, qua đó xác nhận bốn đảm bảo: bí mật chuyển tiếp (lộ khóa hôm nay không làm lộ tin nhắn cũ), xác thực, bí mật sau xâm phạm (thiết bị từng bị lộ tạm thời thì các tin nhắn sau đó vẫn được bảo vệ trở lại) và bí mật của bước bắt tay.
6,5 triệu dòng chứng minh trong 4 tuần, trong khi các dự án kiểm minh trước đó tính bằng năm
Quy trình chia việc giống một nhóm nghiên cứu thật. Các mô hình AI hỗ trợ chuyên gia dịch mục tiêu bảo mật của Signal thành đặc tả toán học, và từng đặc tả đều được con người duyệt. Từ đó các agent chạy bằng Gemini Carbon viết chứng minh bằng Lean, một ngôn ngữ mà trình kiểm tra của nó tự động xác nhận chứng minh có đúng hay không. Khi các agent tự rà soát, chúng chỉ đánh dấu khoảng 1% cơ sở mã cần con người xem kỹ, phần còn lại do Lean kiểm tra.
| Dự án kiểm minh | Công sức ghi nhận |
|---|---|
| Vi hạt nhân seL4 | 20 người-năm |
| Trình biên dịch C CompCert (bản đã kiểm minh) | 6 năm phát triển |
| Mã mật mã cốt lõi của Signal với AlphaProof Code | 4 tuần, đội 5 người, hơn 6 triệu dòng Lean (khoảng 6,5 triệu theo The Register) |
Số liệu: The Register, Google DeepMind. Ba dự án có quy mô và độ khó khác nhau, nên bảng này chỉ cho thấy bậc độ lớn của thời gian, không phải phép so sánh ngang hàng. Chi phí tính toán cũng không nằm trong bảng: nhóm tác giả thừa nhận công việc tiêu tốn khá nhiều token, và Google cũng thừa nhận chưa rõ cách làm này thực dụng đến đâu khi mở rộng.
Để kiểm tra hệ thống phân biệt được mã đúng với mã sai, DeepMind cấy lại hai lỗi thật từng được Signal vá vào một bản mã cô lập. Ở cả hai trường hợp, hệ thống đưa ra chứng minh đã được máy kiểm tra rằng bản có lỗi là không an toàn.
Kết quả đúng trong phạm vi đã chứng minh, chưa phải tấm séc cho cả ứng dụng
Đọc con số “đã kiểm minh Signal” mà bỏ qua phạm vi thì dễ hiểu sai. Phân tích này không kiểm minh toàn bộ ứng dụng Signal trên điện thoại; giao diện, lưu trữ tin nhắn cục bộ và những lớp còn lại của hệ điều hành không nằm trong kết quả. Công trình cũng không phát hiện lỗ hổng mới nào: nó xác nhận rằng giao thức giữ đúng những tính chất đã tuyên bố, chứ không vá được thứ gì chưa biết.
Còn một giới hạn kỹ thuật: kết quả mang tính lý thuyết, vì giả định các thuật toán mật mã bên dưới hoàn hảo và không bảo đảm tính bí mật về mặt tính toán của từng byte. Swarat Chaudhuri, nhà nghiên cứu của DeepMind, cũng nói trước mắt còn “một chặng đường dài” trước khi áp dụng được cho mọi phần mềm. Phía Signal thì đánh giá tích cực: Giám đốc công nghệ Ehren Kret cho rằng cách làm này mở rộng được so với các nỗ lực kiểm minh trước đó vốn chỉ phủ những phần mã nhỏ hơn.
Với người dùng ở Việt Nam, thay đổi nằm ở độ tin cậy chứ không ở thao tác hằng ngày
Signal, Google Messages (khi dùng RCS) và WhatsApp cùng dựa trên giao thức này, nên phần lớn người dùng smartphone ở Việt Nam đang dùng nó dù không biết tên. Kết quả của DeepMind là thêm một lớp bằng chứng độc lập cho thấy thiết kế và mã lõi của giao thức không có kẽ hở logic trong những tính chất đã nêu. Nhưng bản công bố chỉ nói tới mã libsignal; chưa thấy thông tin nào cho biết mã của WhatsApp hay Google Messages đã được đưa vào phạm vi chứng minh, nên không nên đọc đây là chứng nhận cho từng ứng dụng.
Ngoài ra, rủi ro thực tế của đa số người dùng hiếm khi nằm ở bản thân thuật toán mã hóa. Thiết bị bị cài phần mềm độc hại, bản sao lưu không được mã hóa, hay một cuộc lừa đảo khiến người dùng tự đưa mã xác thực cho kẻ gian đều nằm ngoài những gì phép chứng minh này chạm tới. Vì vậy các thói quen như bật khóa màn hình, kiểm tra thiết bị liên kết và không chia sẻ mã xác thực vẫn không thay thế được bằng toán học.
Bước tiếp theo DeepMind nêu là đưa kỹ thuật này vào ngay khâu thiết kế phần mềm, không chỉ cho giao thức mật mã. Theo Chaudhuri, trọng tâm của hướng nghiên cứu sắp tới sẽ là đặc tả, tức việc xác định phần mềm cần bảo vệ điều gì, chứ không còn là bản thân việc chứng minh. DeepMind cũng cho biết đang mở mã nguồn các sản phẩm kiểm minh để cộng đồng kiểm tra lại.
Nguồn tham khảo: Google DeepMind · WIRED · The Register · 9to5Mac
