AI kiểm chứng mã Signal: bằng chứng toán học bảo vệ được đến đâu?

Một ứng dụng nhắn tin có thể vượt qua nhiều phép thử mà vẫn chứa một đường chạy hiếm gặp làm sai cách bảo vệ tin nhắn. Google DeepMind thử tiếp cận vấn đề từ phía khác: xác định bằng toán học những điều mã phải bảo đảm, rồi dùng AI xây dựng chứng minh để một công cụ độc lập kiểm tra. Ngày 10/11/2026, nhóm công bố AlphaProof Code cùng kết quả áp dụng vào mã giao thức Signal. Điều được chứng minh là các thuộc tính cụ thể trong phạm vi nghiên cứu, không phải lời bảo đảm rằng toàn bộ điện thoại hay ứng dụng không thể bị tấn công.

Thử nhiều trường hợp và chứng minh một tính chất khác nhau thế nào?

Hãy lấy ví dụ đơn giản về một hàm chia tiền cho các tài khoản. Chạy thử có thể cho thấy hàm hoạt động đúng với mười hoặc một triệu bộ số. Nhưng nếu một trường hợp rất lớn khiến bộ đếm tràn, các lần thử trước đó không tự loại được khả năng ấy. Kiểm chứng hình thức bắt đầu bằng một mệnh đề rõ ràng, chẳng hạn tổng tiền trước và sau chuyển phải bằng nhau trong những điều kiện đã định. Sau đó, người làm phải chỉ ra mã thực thi thỏa mệnh đề ở mọi trường hợp mà mô hình bao phủ.

Với mật mã, tính chất cần chứng minh khó hơn nhiều so với cân bằng số tiền. Người thiết kế có thể yêu cầu một bên nghe lén không đọc được nội dung, hoặc việc lộ trạng thái ở một thời điểm không làm lộ toàn bộ tin nhắn quá khứ. Bước đầu tiên là diễn đạt chính xác kẻ tấn công được làm gì, biết gì và tiếp cận thiết bị trong hoàn cảnh nào. Nếu mô hình quên cho phép một hành vi thực tế quan trọng, một chứng minh đúng vẫn có thể trả lời một câu hỏi quá hẹp.

AI tìm đường chứng minh, Lean kiểm tra từng bước

Theo Google DeepMind, chuyên gia cùng AI xây đặc tả và con người duyệt các đặc tả đó trước khi nhóm tác nhân AI thực hiện chứng minh. Kết quả được viết bằng Lean, một ngôn ngữ và công cụ kiểm tra chứng minh. Có thể hình dung tác nhân AI như người tìm lời giải, còn bộ kiểm tra là nơi xét từng bước có đi ra từ các quy tắc đã chấp nhận hay không. Một lời giải nghe hợp lý nhưng có bước nhảy sai không được chấp nhận chỉ vì AI trình bày tự tin.

Sự phân công này xử lý một vấn đề quen thuộc của mô hình ngôn ngữ: câu trả lời có thể trôi chảy nhưng sai. AI được phép tìm kiếm, thử và thất bại trên đường xây chứng minh. Điều quyết định không phải lời khẳng định cuối của AI mà là việc bộ kiểm tra chấp nhận toàn bộ chuỗi lập luận theo đặc tả. Khả năng kiểm tra lại khiến đầu ra có giá trị khác với một báo cáo rà mã chỉ viết bằng ngôn ngữ thông thường. Tuy vậy, đặc tả và các thành phần được tin cậy vẫn phải được lựa chọn đúng.

Từ thiết kế giao thức tới mã chạy trên thiết bị

Một giao thức mô tả các bước hai bên trao đổi khóa và bảo vệ tin nhắn. Phần mềm phải biến mô tả đó thành phép toán, bộ nhớ và lệnh máy. Lỗi có thể xuất hiện trong khoảng cách giữa hai tầng: bản thiết kế đúng nhưng mã đọc hoặc cập nhật nhầm trạng thái. Trong báo cáo kỹ thuật, nhóm mô tả kiểm chứng libsignal ở mức mã máy AArch64, kiến trúc lệnh thuộc họ Arm. Công việc bao phủ quá trình bắt tay PQXDH và cơ chế đổi khóa Triple Ratchet với một số thuộc tính bảo mật được nêu rõ.

Google báo cáo quá trình chứng minh kéo dài bốn tuần. Trong một phép kiểm tra riêng, nhóm đưa lại hai lỗi thật đã được sửa vào bản mã cô lập và hệ thống chứng minh được phiên bản đó không thỏa thuộc tính bảo mật. Đây là cách hỏi thêm xem phương pháp có phân biệt được mã có lỗi với mã được chọn để chứng minh hay không. Thời gian bốn tuần là kết quả của đợt nghiên cứu này; nó không có nghĩa mọi chương trình khác có thể được xác minh trong cùng khoảng thời gian hoặc với cùng lượng chuẩn bị.

Điều gì vẫn nằm ngoài bằng chứng?

Báo cáo phân biệt các tầng lập luận, trong đó một tầng dùng mô hình mật mã lý tưởng và một tầng dựa vào các giả định an toàn của những phép toán nền. Người đọc không nên hiểu rằng máy đã thử mọi máy tính có thể xuất hiện trong tương lai để xem có phá được mã hóa hay không. Cũng cần phân biệt phần giao thức với các thành phần khác của một sản phẩm: màn hình hiển thị thông báo, bản sao lưu, quyền truy cập trên thiết bị và cách người dùng xác minh danh tính liên lạc.

Ví dụ, nếu kẻ khác nhìn được màn hình đã mở khóa hoặc điều khiển bàn phím, họ có thể tiếp cận nội dung ở đầu cuối dù phép trao đổi khóa đúng. Đây không phải phản ví dụ cho một định lý chỉ nói về kẻ nghe lén đường truyền; nó là một cách tấn công nằm ở nơi khác. Với đội phần mềm, bước có ích là ghi cạnh mỗi kết quả kiểm chứng ba thứ: phiên bản mã nào, thuộc tính nào, giả định nào. Khi nâng cấp mã hoặc đổi môi trường chạy, đội cần biết phần nào của lập luận còn áp dụng.

AlphaProof Code cho thấy AI có thể đảm nhiệm lượng lớn công việc xây lời giải trong một quy trình có đầu ra kiểm tra được. Chuyên gia vẫn giữ vai trò quyết định câu hỏi cần chứng minh và đọc các giới hạn của câu trả lời. Giá trị thực tế sẽ nằm ở việc nhiều nhóm có thể lặp lại phương pháp trên các phần mã quan trọng, cập nhật bằng chứng khi mã đổi và phát hiện sớm khoảng cách giữa yêu cầu bảo mật với chương trình đang phát hành.

Nguồn: Google DeepMind — công bố ngày 10/11/2026; AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level.

Biểu tượng ứng dụng Signal từ bản năm 2020 — Signal Messenger; dùng minh họa, không thể hiện kết quả kiểm chứng. Trang nguồn và tệp gốc; GPL v3. Dùng nguyên bản.