Google DeepMind dùng các tác tử AI để xác minh mã máy cốt lõi của Signal

Google DeepMind giới thiệu AlphaProof Code vào ngày 10 tháng 11 năm 2026, sử dụng các nhóm tác tử AI để tạo ra những chứng minh Lean được kiểm tra bằng máy về các thuộc tính bảo mật đã xác định của mã libsignal đã biên dịch của Signal. Nhóm nghiên cứu gồm năm người hoàn tất công việc chứng minh trong bốn tuần, đồng thời công bố các đặc tả và hiện vật xác minh để bên ngoài xem xét.

Công trình đã vượt ra khỏi mô hình trừu tượng về thiết kế giao thức của Signal để đi đến phần triển khai đã biên dịch. Các nhà nghiên cứu đưa các crate libsignal v0.105.4 và SPQR v1.6.0 chưa qua chỉnh sửa vào một bộ điều khiển dòng lệnh nhỏ, sau đó dùng rustc nguyên bản để xây dựng một tệp thực thi Linux AArch64 được liên kết tĩnh. Bài báo kỹ thuật mô tả kết quả này là những chứng minh bảo mật cấp giao thức đầu tiên cho mã chưa chỉnh sửa của một phần triển khai giao thức mật mã được sử dụng rộng rãi.

AlphaProof Code phân chia công việc như thế nào

Năm nhà nghiên cứu dành bốn tuần cho công việc chứng minh, liên tục chạy các tác tử trên máy trạm của họ và đồng thời thực hiện các chứng minh ký hiệu lẫn tính toán. Bài báo cho biết các tác tử đã tạo ra khoảng 6,5 triệu dòng mã chứng minh Lean được kiểm tra bằng máy, dựa trên khoảng 26.000 dòng đặc tả đáng tin cậy và ngữ nghĩa AArch64.

Con người lựa chọn các thuộc tính, xử lý những điểm mơ hồ và sự đánh đổi về bảo mật, xem xét các đặc tả và giữ quyền phê duyệt cuối cùng. Các tác tử chạy bằng Gemini 4 Carbon và Claude Opus 5.5 soạn thảo rồi rà soát các đặc tả đó, trong đó có cả việc rà soát bằng một họ mô hình khác. Sau đó, các nhóm tác tử Gemini 4 Carbon tạo ra toàn bộ mã chứng minh; không tác giả nào viết mã chứng minh. Các đợt chạy thông thường sử dụng từ 40 đến 80 tác tử trên một máy trong 24 đến 72 giờ. Một bộ điều phối và các trưởng nhóm phối hợp những tác tử thực hiện chứng minh, trong khi các vai trò kiến trúc sư và tích hợp viên duy trì nền tảng chứng minh dùng chung.

Bộ kiểm soát chỉ chấp nhận một chứng minh sau khi nhân Lean kiểm tra chứng minh đó và một bộ so sánh xác nhận nó khớp với đặc tả đã được giữ kín và con người phê duyệt, bao gồm mọi định nghĩa bắc cầu, đồng thời chỉ sử dụng các tiên đề tiêu chuẩn của Lean. Các tác tử có thể đề xuất những sửa đổi nhỏ khi chứng minh làm lộ ra vấn đề trong đặc tả, nhưng mọi thay đổi đối với các giả định đáng tin cậy đều cần con người phê duyệt hoặc phải tuân theo chính sách do người dùng đặt ra, đồng thời được ghi lại kèm lý do. Cơ chế kiểm soát này xử lý một rủi ro đã được ghi nhận trong các chứng minh do tác tử tạo ra: đặc tả có thể bị làm yếu đi một cách gián tiếp thông qua một trong các định nghĩa của nó.

Phạm vi bảo mật và kiểm thử lỗi trong quá khứ

Mục tiêu được xác minh là mã phiên một-một, bao gồm bắt tay PQXDH và nhắn tin bằng Triple Ratchet. Các nhà nghiên cứu báo cáo hai lập luận độc lập: mười định lý ký hiệu dựa trên các giả định mật mã lý tưởng hóa và một chứng minh tính toán giới hạn lợi thế của kẻ tấn công thông qua các giả định mật mã và các số hạng thống kê. Các thuộc tính được xem xét bao gồm tính bí mật chuyển tiếp, bảo vệ những tin nhắn trước đó nếu trạng thái hiện tại bị đánh cắp; xác thực; bảo mật sau khi bị xâm phạm, tức khả năng khôi phục sau một vụ xâm phạm; và tính bí mật của quá trình bắt tay. Lập luận ký hiệu còn bao gồm tính bí mật của quá trình bắt tay ngay cả sau này khi Diffie–Hellman bị phá vỡ.

Để kiểm tra xem các đặc tả có phát hiện được lỗi thực tế hay không, nhóm đã đảo ngược các bản sửa lỗi của hai lỗi libsignal từng được khắc phục, được gọi là trạng thái yếu và nhóm con nhỏ, rồi biên dịch lại các tệp nhị phân đã bị chỉnh sửa. Trong cả hai trường hợp, nhóm tạo ra các chứng minh Lean cho thấy định lý bảo mật ký hiệu không còn đúng. Kho lưu trữ xác minh công khai phân tách tài liệu về phần tính toán, phần ký hiệu, tệp nhị phân dùng chung và ngữ nghĩa AArch64, đồng thời hướng dẫn cách xây dựng lại và kiểm tra độc lập các chứng minh.

Giám đốc công nghệ của Signal, Ehren Kret, cho biết công trình này “giúp chúng tôi càng thêm tin tưởng vào các bảo đảm về quyền riêng tư của mã nguồn”.

Giới hạn và các bước tiếp theo

Các bảo đảm này còn cách rất xa việc chứng nhận toàn bộ ứng dụng của Signal. Chúng chỉ áp dụng cho bản dựng libsignal-cli của các nhà nghiên cứu khi chạy như một tiến trình mới; việc tạo khóa chưa được xác minh, nhắn tin nhóm được để lại cho công việc tương lai, còn các kênh kề và trạng thái đa thiết bị nằm ngoài kịch bản này. Các nguyên thủy mật mã cấp thấp cùng một số thủ tục đầu ra và thư viện được chọn được biểu diễn bằng các hợp đồng đáng tin cậy, vì vậy kết quả cũng phụ thuộc vào những hợp đồng đó, các đặc tả đã được phê duyệt, nhân Lean, ngữ nghĩa AArch64 và các giả định về những nguyên thủy này.

Bài báo nêu rõ rằng cả hai lập luận đều không chứng minh được khả năng phục hồi hậu lượng tử mà SPQR được thiết kế để bổ sung: định lý tính toán chỉ bao quát kẻ tấn công cổ điển, còn các định lý ratchet ký hiệu cho phép kẻ tấn công chọn khóa SPQR. Mô hình tính toán cũng giới hạn một số hành động của kẻ tấn công và trở nên vô nghĩa khi số lượng tin nhắn và phiên đạt đến những quy mô đủ lớn. Những giới hạn này xác định các yếu tố mà người đánh giá bên ngoài phải tin cậy trước khi xem các chứng minh được kiểm tra bằng máy là bảo đảm an ninh cho một triển khai cụ thể.

Các bước tiếp theo mà nhóm nghiên cứu nêu ra là củng cố các định lý, thu hẹp nền tảng đáng tin cậy bằng cách xác minh thêm các thủ tục được móc nối và kết nối các hợp đồng mật mã với những bản triển khai đã được xác minh, đồng thời mở rộng phạm vi sang nhắn tin nhóm, người gửi ẩn danh và các giao thức phía máy chủ. Mục tiêu xác minh các bản phát hành libsignal mới trước khi phát hành là một mục tiêu nghiên cứu, không phải một kế hoạch triển khai đã được công bố.

Ý nghĩa trước mắt của kết quả này nằm ở sự phân công công việc mà nó thể hiện: các tác tử đảm nhiệm việc xây dựng chứng minh, còn độ tin cậy vẫn dựa trên các đặc tả được con người rà soát và những giả định được nêu rõ. Việc công bố các chứng minh và quy trình kiểm tra giúp những người đánh giá bên ngoài có thể kiểm chứng nền tảng đó, trong khi các nhà nghiên cứu tìm cách đưa quy trình này vào hoạt động phát triển libsignal liên tục.