Google DeepMind dùng AI chứng minh mã hóa Signal an toàn

Giao thức Signal bảo vệ hàng tỉ cuộc trò chuyện riêng tư mỗi ngày, không chỉ trong ứng dụng Signal mà cả trong các biến thể chạy ở WhatsApp, Messenger và Google Messages. Một lỗ hổng duy nhất trong lớp mã hóa có thể phơi bày cùng lúc hàng triệu người, vì vậy giới chuyên gia đã dành nhiều thập kỷ để kiểm chứng giao thức này bằng toán học.

Ngày 10/11/2026, Google DeepMind cho biết họ đã làm được điều chưa ai làm: dùng AlphaProof Code, một hệ thống tác tử AI mới, để chứng minh bằng toán học rằng mã nguồn của giao thức Signal giữ đúng các cam kết bảo mật cốt lõi, xuống tới từng câu lệnh máy chạy trên thiết bị. Toàn bộ quá trình chỉ mất bốn tuần, trong khi trước đây một công việc tương tự thường ngốn nhiều năm của cả đội chuyên gia.

Chứng minh bằng toán học, không chỉ kiểm thử phần mềm

Kiểm thử phần mềm chỉ cho thấy chương trình chạy đúng trong những tình huống đã thử. Kiểm chứng hình thức (formal verification) đi xa hơn: nó chứng minh bằng toán học rằng mã nguồn luôn chạy đúng trong mọi tình huống nằm trong đặc tả, kể cả những trường hợp biên mà người kiểm thử khó nghĩ tới. Đây là tiêu chuẩn đảm bảo cao nhất trong an ninh phần mềm, nhưng cũng tốn công nhất, vì mỗi tính chất đều phải viết lại thành đặc tả toán học rồi chứng minh từng bước.

AlphaProof Code chia công việc đúng như cách một nhóm nghiên cứu vẫn làm. Chuyên gia con người cùng các mô hình AI dịch mục tiêu an ninh của Signal thành đặc tả hình thức, và mọi đặc tả đều có chuyên gia rà soát. Sau đó, các tác tử AI chạy bằng Gemini 4 Carbon đảm nhận phần chứng minh, viết ra hơn 6 triệu dòng mã bằng Lean, ngôn ngữ chuyên dùng để chứng minh tính đúng đắn của mã nguồn bằng máy. Mọi chứng minh đều được hạt nhân của Lean kiểm tra lại tự động.

AI không làm thay con người ở khâu quyết định. Con người quyết định cần chứng minh điều gì, AI thực hiện phần việc nặng nhọc, rồi hệ thống tự rà soát và chỉ ra đúng 1% mã nguồn cần chuyên gia xem lại lần hai.

Bốn tuần thay cho công việc của nhiều năm

Trước AlphaProof Code, hầu hết công việc kiểm chứng giao thức dừng ở mức thiết kế trên giấy. Các chuyên gia chứng minh bản thiết kế thì an toàn, nhưng mã nguồn thật khi biên dịch và chạy trên máy có thể lệch khỏi thiết kế ở những điểm rất nhỏ, và chính những điểm lệch đó là nơi lỗ hổng thực tế thường ẩn náu. AlphaProof Code lấp được khoảng cách này: nó chứng minh mã nguồn đã biên dịch, chứ không chỉ bản thiết kế.

Nhóm nghiên cứu do Pushmeet Kohli và Swarat Chaudhuri dẫn đầu đã làm việc cùng đội ngũ Signal, và theo bài báo kỹ thuật, Claude Opus 5.5 hỗ trợ soạn thảo đặc tả trong khi các tác tử chứng minh chạy trên Gemini 4 Carbon.

Tốc độ là điểm gây ấn tượng nhất. Bốn tuần cho khối lượng chứng minh từng cần nhiều năm không chỉ là chuyện nhanh hơn, mà còn thay đổi hẳn bài toán kinh tế của kiểm chứng hình thức: nếu chi phí đủ thấp, nhiều hệ thống quan trọng khác cũng có thể được chứng minh theo cách này.

Đã chứng minh được những gì, và giới hạn ở đâu

Phạm vi chứng minh được ghi rõ trong bài báo kỹ thuật. Đối tượng là libsignal phiên bản 0.105.4 cùng thư viện spqr 1.6.0, khoảng 560 KB mã nguồn, biên dịch bằng trình biên dịch Rust gốc thành mã máy AArch64 với khoảng 140.000 câu lệnh. Các tính chất đã chứng minh gồm tính bí mật và xác thực của tin nhắn, tính bí mật chuyển tiếp, khả năng an toàn sau khi thiết bị bị xâm nhập, cùng tính bí mật và xác thực của quá trình bắt tay, trong khuôn khổ bắt tay PQXDH và cơ chế Triple Ratchet cho các phiên trò chuyện một-một.

Ngược lại, kết quả không bao phủ trò chuyện nhóm, trạng thái thiết bị liên kết, hệ điều hành hay điện thoại của người dùng, và các thuật toán mã hóa nền tảng được coi là giả thiết chứ không phải đối tượng chứng minh. Bài báo cũng nói rõ chưa có đảm bảo chống lượng tử cho tính chất tự phục hồi của SPQR. Nói cách khác, đây là chứng minh cho lõi mã hóa của giao thức trong một cấu hình cụ thể, không phải giấy chứng nhận toàn bộ ứng dụng Signal không thể bị tấn công.

Thử thách ngược: cố tình cài lại hai lỗi cũ

Để kiểm tra xem hệ thống có thực sự phân biệt được mã đúng và mã sai hay không, nhóm nghiên cứu đã làm một thử thách ngược: cài lại hai lỗi thật từng tồn tại và đã được sửa trong mã nguồn Signal vào một bản sao tách biệt, rồi để AlphaProof Code kiểm chứng bản đó. Trong cả hai trường hợp, hệ thống đều đưa ra chứng minh được máy kiểm tra rằng bản mã chứa lỗi là không an toàn.

Thử thách này trả lời câu hỏi mà mọi hệ thống tự động đều phải đối mặt: liệu nó có đang chứng minh mọi thứ một cách mù quáng hay không. Một hệ thống chỉ biết gật đầu với mã đúng thì chưa đủ tin; nó còn phải biết lắc đầu với mã sai.

Mở mã nguồn và bước tiếp theo

Google DeepMind đã công bố toàn bộ tài liệu kiểm chứng để cộng đồng sử dụng, gồm đặc tả, chứng minh bằng Lean và bản đồ đối chiếu giữa bài báo và mã nguồn, theo giấy phép Apache 2.0. Nhờ đó, các nhà nghiên cứu khác có thể kiểm tra lại từng bước chứng minh thay vì phải tin vào lời khẳng định của DeepMind.

Hướng đi tiếp theo là áp dụng cùng phương pháp cho những hệ thống quan trọng khác, từ firmware thiết bị y tế tới phần mềm lưới điện. DeepMind cũng đặt AlphaProof Code cạnh các tác tử phòng thủ tự động như CodeMender, với lập luận rằng khi kẻ tấn công dùng AI để tìm lỗi nhanh hơn, phía phòng thủ cũng cần công cụ chứng minh tự động để theo kịp.

Với người dùng Signal, WhatsApp, Messenger hay Google Messages, không có bản vá khẩn cấp hay thao tác nào cần làm thêm. Kết quả không sửa một lỗ hổng cụ thể nào, mà xác nhận rằng lõi mã hóa của giao thức, trong phạm vi đã kiểm chứng, đang làm đúng những gì nó hứa hẹn. Đó là tin tốt, nhưng cần đọc đúng mức: niềm tin vào mã hóa vẫn phải đi cùng cập nhật ứng dụng đều đặn và giữ thiết bị luôn được bảo vệ.

Nguồn tham khảo: Google DeepMind