DeepMind dùng AI chứng minh giao thức Signal an toàn

Các nhà nghiên cứu của Google DeepMind vừa dùng AI dạng tác tử (agentic AI) để chứng minh bằng toán học, hay còn gọi là xác minh hình thức (formal verification), nhiều bảo đảm mật mã then chốt của giao thức Signal. Đây là một cột mốc đáng chú ý với cả mật mã học lẫn chính AI, bởi giao thức này đang bảo vệ khối lượng khổng lồ thông tin liên lạc trên toàn thế giới.

Công trình được thực hiện như một dự án thử nghiệm chỉ trong bốn tuần, với sự hỗ trợ của một khung AI mới mang tên AlphaProof Code. Kết quả có ý nghĩa ở hai điểm: nó bổ sung thêm một lớp kiểm chứng độc lập cho giao thức đứng sau Signal, Google Messages và WhatsApp; đồng thời chứng minh năng lực xác minh hình thức của DeepMind khi có AI hỗ trợ.

Xác minh hình thức là gì và vì sao quan trọng

Xác minh hình thức là phương pháp dùng toán học để kiểm tra và chứng minh rằng phần mềm hoạt động đúng như thiết kế, tức là không chứa lỗ hổng nghiêm trọng. Những người ủng hộ phương pháp này từ lâu đã gọi đây là "chén thánh" của an ninh phần mềm.

Trước thời AI, việc này cực kỳ tốn thời gian: con người phải mô tả các đặc tính của phần mềm muốn chứng minh, chuyển các mô tả đó thành công thức, rồi tự xây dựng chứng minh. AI dạng tác tử có thể rút ngắn đáng kể bước cuối cùng, nhờ đó những phân tích như của DeepMind với Signal mới khả thi.

Những gì DeepMind đã làm

Phân tích của DeepMind không phát hiện lỗ hổng mới nào trong phần giao thức Signal được xem xét. Tuy nhiên, khi nhóm nghiên cứu chạy AlphaProof Code trên các phiên bản Signal cũ vốn chứa lỗ hổng đã được biết và đã vá từ lâu, công cụ này đã nhận diện đúng và cho thấy giao thức khi đó không thể được xác minh hình thức.

"Chúng tôi rất phấn khích với kết quả này, nhưng còn một chặng đường dài trước khi có thể mở rộng ra toàn bộ phần mềm của thế giới, và chúng tôi muốn làm được điều đó," Swarat Chaudhuri, nhà khoa học nghiên cứu tại DeepMind, nói với WIRED.

Nhóm nghiên cứu sẽ công bố đặc tả (specification) và bản chứng minh họ xây dựng cho phân tích giao thức Signal, nhằm hỗ trợ các công trình xác minh hình thức khác.

Giới hạn và góc nhìn từ phía Signal

Phân tích này vẫn có phạm vi hạn chế: nó không xác minh hình thức toàn bộ ứng dụng Signal trên di động. Các nhà nghiên cứu DeepMind cũng nhấn mạnh đây chỉ là một cột mốc trong quá trình dài hơn.

Nhóm có được lợi thế khởi đầu nhờ một phần công việc xác minh hình thức mà Quỹ Signal từng thực hiện trước đó. Ehren Kret, giám đốc công nghệ của Signal, nhận xét trong một tuyên bố rằng cách tiếp cận của DeepMind mở rộng đáng kể so với các nỗ lực trước đây vốn chỉ tập trung vào những phần nhỏ của mã nguồn. Theo ông, khi các mối đe dọa an ninh do AI dẫn dắt gia tăng, việc xác minh chặt chẽ việc triển khai giao thức Signal càng củng cố niềm tin vào các bảo đảm riêng tư của mã nguồn.

Câu hỏi mở về chi phí và khả năng mở rộng

Với những dịch vụ quan trọng trong các bối cảnh rủi ro cao, việc xác minh hình thức mọi cơ sở mã và toàn bộ chuỗi cung ứng phần mềm là một mục tiêu đáng mơ ước.

"Nếu giờ bạn có thể xác minh tính đúng đắn của những triển khai này, bạn có thể yên tâm," Pushmeet Kohli, nhà khoa học trưởng của Google Cloud kiêm phó chủ tịch nghiên cứu của DeepMind, nói. "Bạn có thể hình dung các ngân hàng, cùng nhiều công ty khác vốn phụ thuộc vào các bảo đảm và lo lắng về lỗi, giờ có thể nói: 'Tôi có thể chứng minh những thuộc tính này'."

Tuy nhiên, câu hỏi mở với toàn ngành công nghệ là liệu xác minh hình thức tự động bằng AI có thực sự mở rộng được quy mô, và liệu chi phí có khả thi. DeepMind thực hiện phân tích Signal miễn phí như một dự án nghiên cứu; Google từ chối chia sẻ chi phí của phân tích này, cũng không bình luận về việc có kế hoạch ra mắt sản phẩm hay dịch vụ xác minh hình thức thương mại hay không.

Một tiến bộ quan trọng khác mà nhóm nghiên cứu nêu ra là quy trình cộng tác giữa người và AI, cho phép các tác tử đóng góp và tự sửa lỗi ở gần như mọi giai đoạn, trong khi vẫn cần con người tham gia và rà soát ở những điểm mấu chốt.

"Chúng tôi không muốn một thế giới kiểu 'vibe' nơi AI tự đặt ra mục tiêu, AI tự tạo chứng minh và về cơ bản là tự làm bài kiểm tra do chính nó viết ra," Chaudhuri nói. "Có một vùng trung gian."

Góc nhìn

Với các kỹ sư và doanh nghiệp phần mềm, kết quả này cho thấy xác minh hình thức đang dần bước ra khỏi khuôn khổ học thuật nhờ AI rút ngắn khâu xây dựng chứng minh. Những hệ thống xử lý dữ liệu nhạy cảm như ngân hàng, thanh toán hay hạ tầng định danh có thể sớm coi chứng minh hình thức là một lớp bảo đảm bổ sung bên cạnh kiểm thử và rà soát mã.

Tuy vậy, cần tỉnh táo: phân tích của DeepMind mới phủ một phần của một giao thức và chưa phải toàn bộ ứng dụng, chi phí vận hành chưa được công bố, và chưa có sản phẩm thương mại. Các nhóm kỹ thuật có thể chủ động tìm hiểu công cụ chứng minh hình thức và các bộ đặc tả được công bố, nhưng nên xem đây là hướng đầu tư dài hạn cho những thành phần thực sự then chốt thay vì kỳ vọng áp dụng tràn lan ngay lập tức.