Google DeepMind ra mắt AlphaProof Code, xác minh hình thức giao thức Signal

Google DeepMind vừa công bố AlphaProof Code, một khung tác tử (agentic framework) dùng AI để xác minh hình thức (formal verification) — tức chứng minh bằng toán học rằng mã nguồn chạy đúng và không có lỗi — ở độ sâu chưa từng có. Thành tựu đầu tiên: các tác tử AI do DeepMind dẫn dắt đã chứng minh được các thuộc tính bảo mật then chốt trong mã nguồn thực tế của giao thức Signal, công nghệ bảo vệ hàng tỷ cuộc trò chuyện riêng tư trên các ứng dụng như Signal và Google Messages.

Đây là lần đầu tiên AI được sử dụng để xác minh hình thức một giao thức mật mã đang được triển khai rộng rãi ở mức độ này. Đồng thời, đây cũng là lần đầu tiên phần triển khai (implementation) của một giao thức như vậy được xác minh hình thức bằng bất kỳ phương pháp nào, có AI hay không có AI.

Minh họa xác minh hình thức mã nguồn bằng AI

Cách AlphaProof Code xác minh Signal

AlphaProof Code là một khung tác tử đa mô hình ngôn ngữ lớn (multi-LLM) chia công việc xác minh hình thức theo cách một nhóm nghiên cứu vẫn làm: chuyên gia con người cùng AI quyết định cần chứng minh điều gì, còn một nhóm tác tử AI thực hiện việc chứng minh.

• Đầu tiên, các nhà nghiên cứu phối hợp với nhiều mô hình khác nhau để chuyển các mục tiêu bảo mật của Signal thành đặc tả toán học hình thức, với chuyên gia con người rà soát từng đặc tả.
• Tiếp đó, các tác tử chạy trên Gemini Carbon thực hiện chứng minh, tạo ra hơn sáu triệu dòng Lean — ngôn ngữ lập trình dùng để chứng minh chính xác về mặt toán học tính đúng đắn của mã.
• Sau đó, các tác tử tự kiểm tra lại bản chứng minh và đánh dấu những vùng cần con người xem xét kỹ — chỉ chiếm 1% khối mã, tiết kiệm rất nhiều thời gian. Vì Lean tự động kiểm tra phần còn lại, các chuyên gia có thể tập trung vào nơi cần phán đoán của con người nhất.

Vượt ra ngoài mức thiết kế

Các giao thức mật mã là nền tảng của gần như mọi liên lạc số, từ ngân hàng trực tuyến đến duyệt web, và chỉ một lỗi duy nhất có thể phơi bày hàng triệu người cùng lúc. Đó là lý do các chuyên gia đã dành nhiều thập kỷ phân tích hình thức các giao thức này.

Tuy nhiên, phần lớn việc xác minh giao thức chỉ dừng ở mức thiết kế. Các tác tử của DeepMind đi xa hơn: chứng minh rằng mã đã biên dịch đáp ứng các thuộc tính bảo mật then chốt — chẳng hạn giữ tin nhắn được bảo vệ trước và sau khi thiết bị bị xâm phạm tạm thời — xuống tận đoạn mã chính xác chạy trên thiết bị.

Vì lỗ hổng trong thực tế thường ẩn trong khoảng cách giữa thiết kế và triển khai, việc bắc cầu khoảng cách này khiến các chứng minh phức tạp hơn rất nhiều. Dù vậy, quá trình xác minh chỉ mất bốn tuần — công việc mà các nhóm chuyên gia thường phải mất nhiều năm.

Quy trình tác tử AI tạo và kiểm tra chứng minh Lean

Kiểm chứng bằng lỗi thật

Để xác nhận AlphaProof Code có thể phân biệt mã đúng với mã lỗi, nhóm nghiên cứu đã đưa hai lỗi thật, từng được sửa trước đó, trở lại một phiên bản tách biệt của mã Signal. Ở cả hai trường hợp, hệ thống đều tạo ra chứng minh được máy kiểm tra rằng phiên bản lỗi là không an toàn.

Trong AlphaProof Code, các tác tử AI hỗ trợ người dùng viết đặc tả, sau đó tự động chứng minh rằng phần triển khai đáp ứng đặc tả đó. Mọi chứng minh đều được Lean kiểm tra để xác thực công việc của các tác tử.

"Dù các công trình xác minh hình thức trước đây buộc phải tập trung vào phạm vi nhỏ hơn, cách tiếp cận mới này cho phép mở rộng đáng kể. Việc dùng tác tử AI để tự động chuyển mã đang chạy thành các định lý Lean hợp lệ là một bước đột phá lớn. 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ẽ giao thức Signal bằng chứng minh định lý tự động giúp chúng tôi càng tin tưởng hơn rằng mã nguồn thực sự mang lại các bảo đảm về quyền riêng tư."

— Ehren Kret, Giám đốc Công nghệ của Signal

Tương lai của bảo mật

Việc giải quyết thách thức lâu năm này cho thấy AI có thể mang mức bảo đảm an ninh cao cấp đến cho doanh nghiệp, chính phủ và hạ tầng trọng yếu, qua đó giúp phòng thủ trước các mối đe dọa mạng do tác tử AI gây ra.

Xác minh phần mật mã lõi của Signal đặt nền móng để bảo vệ các hệ thống quan trọng khác, từ firmware thiết bị y tế đến phần mềm lưới điện. Quy mô hóa các kỹ thuật này vẫn cần nghiên cứu tiếp. Khi kết hợp với các tác tử phòng thủ tự động như CodeMender, xác minh hình thức có thể giúp đối phó tốc độ và quy mô của các mối đe dọa mạng hiện đại, hướng tới phần mềm có chứng minh toán học rằng các biện pháp bảo vệ hoạt động đúng.

Google DeepMind cho biết sẽ mở mã nguồn các sản phẩm xác minh hình thức của mình để cộng đồng sử dụng.

Đội ngũ nghiên cứu xác minh hình thức của Google DeepMind

Góc nhìn

Điểm đáng chú ý nhất với giới kỹ sư phần mềm không nằm ở con số sáu triệu dòng Lean, mà ở việc AI được dùng để rút ngắn khoảng cách giữa bản thiết kế và mã chạy thật — nơi phần lớn lỗ hổng thực tế trú ngụ. Mô hình làm việc "chuyên gia con người đặt mục tiêu, tác tử AI làm chứng minh, Lean kiểm tra tự động, con người chỉ rà soát 1% khối mã" là một cách phân chia lao động mà các nhóm kỹ thuật Việt Nam có thể tham khảo khi bắt đầu áp dụng trợ lý AI vào quy trình kiểm thử và đảm bảo chất lượng.

Tuy vậy, xác minh hình thức vẫn là kỹ thuật đòi hỏi chuyên môn cao về logic và ngôn ngữ chứng minh như Lean, và mới được chứng minh trên một giao thức cụ thể chứ chưa phải quy trình phổ thông. Với các đội phát triển sản phẩm liên quan đến thanh toán, dữ liệu cá nhân hay thiết bị kết nối, đây là tín hiệu nên theo dõi: khi các sản phẩm xác minh hình thức được mở mã nguồn, chi phí tiếp cận công nghệ này sẽ giảm dần, và yêu cầu về bằng chứng toán học cho các thành phần bảo mật then chốt có thể trở thành tiêu chuẩn mới.