AI tạo 6,5 triệu dòng mã chứng minh để kiểm tra giao thức Signal

Google DeepMind đã dùng các tác nhân AI để kiểm chứng bằng toán học những thuộc tính bảo mật cốt lõi trong mã xử lý hội thoại riêng giữa hai người của giao thức mã hóa Signal. Phân tích kéo dài 4 tuần, nhưng không kiểm chứng tin nhắn nhóm hay toàn bộ ứng dụng Signal.

Google DeepMind công bố kết quả nghiên cứu AlphaProof Code ngày 10 trên blog chính thức và trong bài báo kỹ thuật cùng tài liệu chứng minh. AlphaProof Code là một khung kiểm chứng hình thức, trong đó các tác nhân AI xây dựng chứng minh cho mã thực tế dựa trên những điều kiện bảo mật do con người đặt ra.

Kiểm chứng hình thức khác với thử nghiệm bằng cách đưa một số đầu vào vào mã để tìm lỗi. Phương pháp này biểu diễn các điều kiện mà mã phải tuân thủ bằng toán học, rồi chứng minh kết quả thực thi có đáp ứng các điều kiện đó hay không.

Nhóm nghiên cứu để con người xác định thuộc tính bảo mật cần chứng minh, đồng thời soạn và rà soát đặc tả. Chứng minh do tác nhân AI tạo ra chỉ được chấp nhận nếu vượt qua bộ kiểm tra của Lean; kết luận không dựa riêng vào đánh giá của tác nhân.

Đối tượng kiểm chứng là tệp thực thi dành cho hội thoại riêng giữa hai người, được xây dựng bằng libsignal 0.105.4 và SPQR 1.6.0. Nhóm nghiên cứu bọc các thư viện chưa chỉnh sửa bằng một công cụ dòng lệnh, sau đó biên dịch thành mã máy AArch64 để phân tích.

Các chức năng được kiểm tra gồm PQXDH, giao thức thống nhất khóa mã hóa khi bắt đầu hội thoại, và Triple Ratchet, cơ chế cập nhật khóa sau mỗi tin nhắn. Họ giao thức Signal cũng được sử dụng trong Google Messages, WhatsApp và Meta Messenger.

Bài báo nêu các thuộc tính nằm trong phạm vi chứng minh gồm tính bí mật chuyển tiếp, nhằm ngăn tin nhắn cũ bị lộ khi khóa bị tiết lộ về sau; bảo mật sau khi bị xâm phạm, tức khả năng khôi phục bảo vệ sau khi khóa lộ; xác thực đối tác và tính bí mật của kết nối ban đầu. Tính bảo mật và tính xác thực của tin nhắn cũng nằm trong các hạng mục kiểm tra.

Nhóm nghiên cứu đưa ra kết quả theo cả mô hình ký hiệu và mô hình tính toán. Mô hình ký hiệu xem các phép toán mật mã là những đối tượng lý tưởng, còn mô hình tính toán phân tích thuộc tính bảo mật với giả định kẻ tấn công có năng lực tính toán giới hạn.

Phạm vi bảo đảm của hai mô hình không giống nhau. Mô hình ký hiệu xem xét tính bí mật của kết nối ban đầu ngay cả trong trường hợp kẻ tấn công lượng tử phá được trao đổi khóa Diffie–Hellman. Mô hình tính toán không xét kẻ tấn công lượng tử; khả năng khôi phục của SPQR trước tấn công lượng tử cũng nằm ngoài phạm vi chứng minh.

Nghiên cứu đối chiếu đặc tả với hành vi của tệp thực thi đã biên dịch, thay vì chỉ dừng ở tài liệu thiết kế giao thức. Tuy nhiên, đối tượng được chứng minh không phải tệp thực thi của ứng dụng Signal mà là công cụ dòng lệnh do nhóm nghiên cứu tạo ra.

Kết quả dựa trên một số giả định. Nhóm nghiên cứu giả định các phép toán mật mã và một số chức năng thư viện hoạt động theo những điều kiện đã quy định trong hợp đồng. Bộ kiểm tra Lean và mô hình ngữ nghĩa AArch64 cũng thuộc cơ sở tin cậy của nghiên cứu.

Phạm vi kiểm chứng chỉ gồm hội thoại giữa hai người. Nhắn tin nhóm, trạng thái trên nhiều thiết bị và bản thân ứng dụng Signal đều không nằm trong phạm vi; nhóm nghiên cứu nêu rõ đây là giới hạn của nghiên cứu.

Để kiểm tra phương pháp có phát hiện được sai sót hay không, nhóm nghiên cứu đưa hai lỗi đã được phát hiện và sửa trước đó trở lại các đoạn mã được cô lập. Cả hai trường hợp đều cho kết quả kiểm chứng bằng máy rằng mệnh đề bảo mật không成立; nghiên cứu không phát hiện lỗ hổng mới.

Năm thành viên nhóm nghiên cứu làm việc song song trong 4 tuần và tạo khoảng 6,5 triệu dòng mã chứng minh Lean. Bài báo cho biết các đặc tả tin cậy cần thiết cho chứng minh cùng mô hình ngữ nghĩa AArch64 dài khoảng 26.000 dòng.

Ehren Kret, Giám đốc công nghệ (CTO) của Signal, nói: “Kiểm chứng hình thức trước đây tập trung vào những phần nhỏ của mã, còn cách tiếp cận của Google DeepMind mở rộng đáng kể phạm vi đó”. Nhận xét này đánh giá việc nghiên cứu kiểm chứng cách triển khai giao thức trên phạm vi rộng hơn.

WIRED nhận định chưa rõ nghiên cứu đã giải quyết được bài toán mở rộng quy mô và chi phí trong ứng dụng thực tế của kiểm chứng hình thức có AI hỗ trợ hay chưa. Google chưa công bố chi phí phân tích hoặc kế hoạch ra mắt sản phẩm, dịch vụ kiểm chứng thương mại.

Bài báo đề xuất kiểm chứng tin nhắn nhóm, tính năng ẩn danh tính người gửi và giao thức phía máy chủ trong các nghiên cứu tiếp theo. Google DeepMind đã công bố đặc tả và tài liệu chứng minh.