Google DeepMind cho biết đã xác minh hình thức mã máy của giao thức Signal bằng AlphaProof Code

Pushmeet Kohli của Google DeepMind thông báo rằng nhóm của ông đã chứng minh các thuộc tính bảo mật then chốt của mã máy làm nền tảng cho giao thức nhắn tin Signal. DeepMind cho biết đây là lần đầu tiên mã sản xuất của một giao thức được triển khai rộng rãi được xác minh hình thức ở độ sâu này bằng bất kỳ phương pháp nào. Đây là những tuyên bố của chính DeepMind.

Công trình sử dụng AlphaProof Code, được DeepMind mô tả là một khung tác tử mới để xác minh hình thức, chạy trên các LLM, trong đó có Gemini Carbon. DeepMind cho biết quá trình xác minh đi sâu đến tận mã chạy trên thiết bị và mất khoảng một tháng, trong khi những nỗ lực tương tự có thể đòi hỏi hàng chục năm công sức cộng gộp của nhiều nhóm. DeepMind ghi nhận nhóm Signal là đối tác.

DeepMind đang phát hành mã nguồn mở các đặc tả hình thức và tạo tác xác minh để những người khác có thể tiếp tục phát triển dựa trên đó. Bài đăng nhận được 1.297 lượt thích trên X tính đến sáng ngày 10 tháng 11.