Google DeepMind chứng minh mã hóa của Signal và WhatsApp hoàn toàn an toàn

Giao thức Signal từ lâu đã được coi là tiêu chuẩn vàng cho tính năng nhắn tin mã hóa đầu cuối, với những nhân vật nổi tiếng như Edward Snowden từng lên tiếng ủng hộ. Giờ đây, một phân tích từ Google DeepMind đã "xác minh chính thức" mức độ an toàn của giao thức này. Bên cạnh việc được sử dụng trong ứng dụng Signal, giao thức tương tự cũng được dùng bởi WhatsApp và Google Messages, và công trình này được mô tả là "một bước phát triển mang tính bước ngoặt". "Xác minh hình thức" là thuật ngữ dùng để chỉ việc chứng minh hoặc bác bỏ bằng toán học rằng một thuật toán hoặc giao thức mật mã đáp ứng các tuyên bố bảo mật của nó trong mọi điều kiện. Nó đảm bảo rằng không có tình huống nào mà giao thức có thể thất bại. Đây là một tiêu chuẩn cao hơn nhiều so với các phương pháp kiểm thử truyền thống vốn chỉ cố gắng tìm ra các lỗ hổng nhưng không thể hứa hẹn rằng sẽ không còn lỗ hổng nào khác tồn tại. Việc sử dụng AI tác tử để thực hiện xác minh hình thức là một bước đột phá lớn đối với cả ngành mật mã học lẫn trí tuệ nhân tạo. Tuy nhiên, phương pháp này đòi hỏi năng lực tính toán cực lớn, vì vậy Google chia sẻ với trang Wired rằng vẫn chưa rõ liệu việc ứng dụng nó rộng rãi hơn có mang tính thực tế hay không. Các nhà nghiên cứu của DeepMind nhấn mạnh rằng phát hiện của họ chỉ là một cột mốc trong một tiến trình lớn hơn. Swarat Chaudhuri, một nhà nghiên cứu tại DeepMind, chia sẻ với WIRED: "Chúng tôi rất hào hứng với kết quả này, nhưng vẫn còn một chặng đường dài trước khi có thể mở rộng quy mô này cho toàn bộ phần mềm trên thế giới, và đó là điều chúng tôi muốn làm". Điều quan trọng cần lưu ý là việc xác thực này dành cho chính giao thức chứ không phải toàn bộ ứng dụng Signal nói chung. Tuy nhiên, người dùng có thể phần nào yên tâm khi biết rằng khi thử nghiệm với các phiên bản cũ của Signal từng chứa lỗ hổng đã biết, hệ thống đã nhận diện và gắn cờ chúng là không đạt yêu cầu xác minh hình thức. Cũng cần nói thêm rằng Google đã có thể dựa trên một số công trình xác minh hình thức trước đây từng được hoàn thành mà không cần sự trợ giúp của AI. Quá trình phân tích này mất bốn tuần và quy mô tài nguyên cần thiết vẫn chưa được công bố, vì vậy chúng ta không nên kỳ vọng hàng loạt giao thức khác sẽ được xác thực một cách nhanh chóng. Dù vậy, đây vẫn là một vấn đề rất lớn.