Mã hóa của Signal vượt qua bản chứng minh toán học 6,5 triệu dòng do AI viết

Mã hóa của Signal giờ đây có một điều mà hầu như không phần mềm phổ biến nào có thể khẳng định: một chứng minh toán học cho thấy nó làm đúng những gì đã cam kết. Một nhóm tác nhân AI đã phân tích libsignal, thư viện vận hành giao thức Signal, và chứng minh rằng các cuộc trò chuyện riêng tư giữa hai người vẫn được giữ kín, xác thực đúng người ở đầu bên kia và có thể ngăn kẻ tấn công truy cập trở lại sau khi khóa bị đánh cắp. Họ không phát hiện lỗ hổng mới nào.

Kết quả này có ý nghĩa vượt xa phạm vi người dùng Signal. Giao thức này là tiêu chuẩn toàn cầu cho nhắn tin mã hóa đầu cuối, và các biến thể của nó bảo vệ những cuộc trò chuyện trên WhatsApp, Messenger và Google Messages. Việc kiểm tra mã đã triển khai thực tế ở mức độ sâu như vậy vốn chậm đến mức hầu như chẳng ai thử: một trong những thành tựu lớn nhất của lĩnh vực này, xác minh một nhân hệ điều hành, tiêu tốn công sức tương đương 20 người làm trong một năm. Công việc lần này chỉ mất bốn tuần.

Công cụ do Google DeepMind xây dựng có tên AlphaProof Code. Trước tiên, các chuyên gia và mô hình AI chuyển những mục tiêu bảo mật của Signal thành các mệnh đề hình thức trong Lean, một ngôn ngữ lập trình được thiết kế cho chứng minh toán học, và con người rà soát từng mệnh đề. Sau đó, các nhóm gồm 40 đến 80 tác nhân, vận hành bằng Gemini Carbon, viết các chứng minh, mỗi lần chạy liên tục từ 24 đến 72 giờ trên một máy duy nhất. Kết quả là khoảng 6,5 triệu dòng Lean.

Không ai cần phải tin vào từng dòng trong số hàng triệu dòng đó. Nhân Lean kiểm tra mọi bước và loại bỏ mọi chứng minh không hợp lệ, nên mô hình nào viết ra hay mắc lỗi bao nhiêu lần trong quá trình thực hiện cũng không làm thay đổi kết quả. Điều con người thực sự phải tin cậy ít hơn nhiều: khoảng 26.000 dòng đặc tả và một mô hình mô phỏng cách bộ xử lý ARM thực thi mã.

Các chứng minh bao quát những phần của Signal bảo vệ một cuộc trò chuyện: bước bắt tay PQXDH để thiết lập cuộc trò chuyện và Triple Ratchet, cơ chế thay khóa sau mỗi tin nhắn, bao gồm cả lớp hậu lượng tử được thiết kế để chống lại các máy tính lượng tử trong tương lai. Trên thực tế, điều đó có nghĩa là đánh cắp khóa hiện tại trên điện thoại không giúp mở được những tin nhắn cũ, còn kẻ trộm sẽ mất quyền truy cập trở lại sau khi hai bên trao đổi khóa mới.

Để chứng minh hệ thống có thể phân biệt mã tốt với mã lỗi, các nhà nghiên cứu đã đưa trở lại libsignal hai lỗi cũ vốn đã được khắc phục. Một lỗi khiến thư viện giữ lại bản sao của khóa bí mật mà lẽ ra phải xóa. Trong cả hai trường hợp, AlphaProof Code đều tạo ra một chứng minh được máy kiểm tra, xác nhận phiên bản có lỗi là không an toàn.

Những giới hạn của công trình là có thật. Chứng minh chỉ bao quát các phiên liên lạc giữa hai người; DeepMind cho biết nhắn tin nhóm là hướng nghiên cứu trong tương lai. Kết quả áp dụng cho libsignal phiên bản 0.105.4, được biên dịch bằng trình biên dịch Rust tiêu chuẩn dành cho ARM Linux bên trong một chương trình thử nghiệm nhỏ, chứ không phải toàn bộ ứng dụng Signal trên iPhone, Android hay máy tính. Các khối nền tảng mật mã cấp thấp được giả định là an toàn, chứ không được chứng minh. Sai sót trong các đặc tả do con người phê duyệt sẽ làm suy yếu mức bảo đảm; hơn nữa, WhatsApp và các ứng dụng khác sử dụng phiên bản giao thức riêng, nên kết quả này không tự động áp dụng cho họ. Google cũng từ chối cho Wired biết chi phí phân tích là bao nhiêu hoặc liệu hãng có định bán công cụ này dưới dạng dịch vụ hay không.

Signal hoan nghênh kết quả. “Khi các mối đe dọa an ninh do AI thúc đẩy ngày càng gia tăng, việc xác minh nghiêm ngặt phần triển khai giao thức Signal giúp chúng tôi càng tin tưởng hơn vào những bảo đảm về quyền riêng tư của mã nguồn”, Ehren Kret, giám đốc công nghệ của Signal, cho biết trong một tuyên bố. Swarat Chaudhuri, nhà khoa học nghiên cứu tại DeepMind, thận trọng hơn; ông nói với Wired rằng vẫn còn “một chặng đường dài” trước khi phương pháp này có thể mở rộng “ra toàn bộ phần mềm trên thế giới”.

Người dùng Signal không cần cài đặt gì hay thay đổi thiết lập nào. Chứng minh này áp dụng cho mã đã có sẵn trong ứng dụng.

DeepMind công bố công trình vào ngày 10 tháng 11, kèm theo một bài báo kỹ thuật, đồng thời phát hành các đặc tả và chứng minh dưới dạng mã nguồn mở trên GitHub. Hãng xem dự án Signal là một cột mốc hướng tới mục tiêu lớn về xác minh hình thức được đề ra hồi tháng 4, đồng thời nêu phần mềm nhúng trong thiết bị y tế và phần mềm lưới điện là những hệ thống muốn kiểm tra tiếp theo.

Chaudhuri cũng vạch rõ giới hạn về mức độ công việc nên giao cho máy móc. “Chúng tôi không muốn rơi vào một thế giới kiểu ‘vibe’ này, nơi AI tạo ra mục tiêu và cũng chính AI tạo ra các chứng minh”, ông nói với Wired. Con người vẫn quyết định điều gì được xem là an toàn; AI chỉ chứng minh điều đó.

Thẻ: an ninh mạng, Google DeepMind, AlphaProof Code, kiểm chứng hình thức, libsignal, mã hóa đầu cuối