AlphaProof Code: AI chứng minh đặc tính bảo mật mã của Signal
· Ban biên tập BehindLines
Các nhà nghiên cứu của Google DeepMind cho biết họ đã dùng các tác tử trí tuệ nhân tạo để chứng minh nhiều bảo đảm an ninh của mã thật mà giao thức nhắn tin Signal dựa vào. Theo bài đăng của DeepMind, đây sẽ là lần đầu tiên một AI kiểm chứng hình thức, ở mức chi tiết như vậy, một giao thức mật mã được dùng rộng rãi; The Register cho biết đó là điều các nhà nghiên cứu tuyên bố.
Một phương pháp làm theo nhóm
Hệ thống có tên AlphaProof Code. Theo DeepMind, các chuyên gia con người cùng nhiều mô hình ngôn ngữ trước hết biến mục tiêu bảo mật của Signal thành các đặc tả toán học, và có người xem xét từng đặc tả một. Sau đó các tác tử viết chứng minh bằng Lean, một ngôn ngữ mà bộ kiểm tra của nó tự động xác nhận các suy luận. Theo The Register, các tác tử đã tạo ra 6,5 triệu dòng Lean; DeepMind nói là hơn 6 triệu. Tiếp đó chúng kiểm toán các chứng minh này và đánh dấu khoảng 1% mã để con người xem lại lần nữa, điều mà DeepMind cho là tiết kiệm rất nhiều thời gian.
Những gì đã được chứng minh
DeepMind nhấn mạnh rằng các chứng minh nhắm vào mã đã biên dịch, chứ không chỉ sơ đồ lý thuyết của giao thức. Chúng bao gồm, chẳng hạn, việc bảo vệ tin nhắn trước và sau khi một thiết bị bị xâm nhập tạm thời. The Register còn nhắc đến tính bí mật về sau, xác thực và tính bí mật của lần trao đổi khóa ban đầu. Để chắc rằng phương pháp phân biệt được mã đúng với mã có lỗi, nhóm đã đặt lại hai lỗi thật, đã được sửa, vào một bản cô lập của mã Signal; lần nào hệ thống cũng đưa ra bằng chứng do máy xác nhận rằng bản đó không an toàn.
Những giới hạn được thừa nhận
The Register nêu rõ kết quả vẫn mang tính lý thuyết: nó xuất phát từ mật mã học được giả định là hoàn hảo và không bảo đảm tính bí mật tính toán của các byte. Theo các tác giả mà trang này trích dẫn, công việc kéo dài bốn tuần với năm người và tiêu tốn "khá nhiều token". Họ nhắc rằng việc kiểm chứng vi nhân seL4 tốn 20 người-năm và trình biên dịch CompCert cần sáu năm phát triển.
Ehren Kret, giám đốc công nghệ của Signal, nói trong bài đăng của DeepMind rằng cách tiếp cận này mở rộng rõ rệt phạm vi của kiểm chứng hình thức. Swarat Chaudhuri, một trong các nhà nghiên cứu, nói với The Register rằng khó khăn tiếp theo sẽ là quyết định cần đặc tả điều gì, hơn là việc tạo ra các chứng minh.
Vì sao điều này quan trọng
DeepMind lưu ý rằng các lỗ hổng thực tế thường nằm ở khoảng cách giữa thiết kế và triển khai của một giao thức, khoảng cách mà các chứng minh này muốn thu hẹp. Công ty thấy đây là nền tảng để bảo vệ những hệ thống thiết yếu khác, như phần sụn thiết bị y tế hay phần mềm lưới điện, đồng thời nói rõ rằng việc mở rộng quy mô vẫn cần thêm nghiên cứu.