Google DeepMind dùng AI kiểm chứng bảo mật Signal
"Google DeepMind used its AlphaProof Code framework, combining human guidance and AI agents, to formally verify the security of Signal's post-quantum PQXDH handshake and Triple Ratchet protocols. This verification validates Signal's forward secrecy, authentication, and security properties at the machine-code level, representing a significant step towards scalable formal verification of cryptographic implementations. The project involved generating and auditing 6.5 million lines of Lean code."
Việc xác minh chính thức các giao thức mã hóa như PQXDH và Triple Ratchet giúp tăng cường bảo mật cho ứng dụng Signal. Điều này đặc biệt quan trọng trong bối cảnh các cuộc tấn công mạng ngày càng tinh vi.
Các doanh nghiệp Việt Nam sử dụng Signal hoặc các ứng dụng mã hóa tương tự có thể giảm thiểu rủi ro về bảo mật thông tin. Tuy nhiên, cần lưu ý rằng đây chỉ là một bước trong quá trình đảm bảo an toàn cho hệ thống.
Google DeepMind đã dùng AlphaProof Code, kết hợp hướng dẫn từ người và AI, để xác minh chính thức bảo mật của Signal. Họ tập trung vào giao thức PQXDH (post-quantum) và Triple Ratchet, hai thành phần quan trọng của Signal. Việc này xác nhận các tính chất bảo mật của Signal ở cấp độ mã máy.
Đây là lần đầu tiên AI hỗ trợ tạo ra bằng chứng liên kết bảo mật giao thức với một ứng dụng mã hóa phổ biến. Dự án tạo ra và kiểm tra 6.5 triệu dòng mã Lean.
AlphaProof Code hoạt động bằng cách biến mục tiêu bảo mật của Signal thành thông số toán học. Sau đó, các agent Gemini Carbon tạo mã Lean để chứng minh tính đúng đắn của libsignal. Con người rà soát và chỉnh sửa những phần AI cần hỗ trợ. Kết quả này giả định mã hóa hoàn hảo, nhưng vẫn là một bước tiến quan trọng.
Swarat Chaudhuri, nhà khoa học tại Google DeepMind, cho biết hệ thống này được xây dựng để cộng tác giữa người và AI. Ông nhấn mạnh việc xác định điều cần chứng minh là khó khăn hơn việc chứng minh nó. Formal verification (xác minh hình thức) từng tốn nhiều công sức, ví dụ như seL4 microkernel mất 20 năm công sức, CompCert C compiler mất 6 năm. AlphaProof Code có thể giảm chi phí này, dù dự án Signal vẫn cần 4 tuần và “khá nhiều token”.
DeepMind đang phát triển AlphaProof Nexus, tập trung vào toán học, và muốn áp dụng công nghệ này trong quá trình thiết kế phần mềm, không chỉ cho giao thức mã hóa. Họ tin rằng việc xác định thông số bảo mật (specification) là bước tiếp theo quan trọng.
Câu hỏi thường gặp
AlphaProof Code là gì?
AlphaProof Code là framework của Google DeepMind, kết hợp hướng dẫn của con người và AI để xác minh chính thức bảo mật phần mềm. Nó sử dụng Lean, một ngôn ngữ chứng minh, để tạo và kiểm tra các bằng chứng về tính đúng đắn của mã.
Signal được xác minh những gì?
AlphaProof Code xác minh giao thức PQXDH (post-quantum) và Triple Ratchet của Signal. Điều này xác nhận các tính chất như forward secrecy (bảo mật chuyển tiếp), authentication (xác thực) và post-compromise security (bảo mật sau xâm nhập).
Quá trình xác minh mất bao lâu?
Dự án xác minh Signal mất 4 tuần với một đội ngũ 5 người và sử dụng một lượng lớn tài nguyên tính toán (được gọi là 'tokens'). Nó tạo ra 6.5 triệu dòng mã Lean.
Góc nhìn của Orange Cloud
Theo chúng tôi, việc DeepMind sử dụng AI để xác minh bảo mật Signal cho thấy tiềm năng lớn trong việc tăng cường an ninh cho các ứng dụng mã hóa. Các doanh nghiệp Việt Nam sử dụng Signal hoặc các ứng dụng tương tự có thể hưởng lợi từ các phương pháp xác minh tự động này. Tuy nhiên, cần lưu ý rằng kết quả này dựa trên giả định về mã hóa hoàn hảo và chưa giải quyết được các lỗ hổng tiềm ẩn khác. Điều đáng chú ý là việc tập trung vào specification (xác định thông số) có thể là hướng đi quan trọng để phát triển các hệ thống bảo mật an toàn hơn.