AlphaProof Code và Tín hiệu: các bằng chứng bảo mật mã máy đã được kiểm tra và các giả định đáng tin cậy

Nội dung video này đề cập

• Các tác nhân AI tạo ra các bằng chứng ứng cử viên; hạt nhân của Lean kiểm tra xem chúng có thiết lập được yêu cầu chính thức đã được con người phê duyệt hay không.
• Mục tiêu đã được xác minh là một bộ khung CLI libsignal đã biên dịch cụ thể, với ngữ nghĩa đáng tin cậy và các hợp đồng mật mã.
• Việc chứng minh nhị phân đã biên dịch loại bỏ trình biên dịch Rust khỏi cơ sở đáng tin cậy cho các thuộc tính đã nêu của nhị phân đó.
• Các nhà nghiên cứu báo cáo hai lần tái tạo lại riêng biệt các lỗi đã được sửa trước đó vi phạm định lý bảo mật tượng trưng của họ.
• Trình so sánh kiểm tra định lý và mọi định nghĩa phụ thuộc so với đặc tả đã được phê duyệt được bảo vệ; các sửa đổi được thông qua một quy trình xem xét riêng biệt.

Bản ghi đã dịch

Được dịch từ lời tường thuật tiếng Anh gốc. Âm thanh và phụ đề có sẵn được điều khiển bởi YouTube.

Ai kiểm tra bằng chứng bảo mật AI?

0:00 Kiểm toán bảo mật AI vẫn nghe có vẻ như tin tưởng một chatbot. Kết quả Signal mới của Google đi kèm với các bằng chứng toán học của một hạt nhân riêng biệt kiểm tra. Trong video này, Google đã chứng minh điều gì? Và làm thế nào họ ngăn chặn một tác nhân thay đổi các mục tiêu? Đây là câu trả lời hữu ích. Các mô hình viết các bằng chứng ứng cử viên, và Lean kiểm tra các bằng chứng so với một yêu cầu đã được con người phê duyệt về mã đã biên dịch được chọn. Con người vẫn sở hữu yêu cầu và các giả định.

0:21 Bạn có thể kiểm tra kết quả mà không cần tin vào bài phát biểu chiến thắng của mô hình. Một kiểm tra riêng biệt nắm bắt việc thay đổi câu hỏi một cách lặng lẽ. Chúng ta sẽ đi sâu vào các định nghĩa. Hôm nay là thứ Ba, ngày mười tháng Mười một, và đây là The Daily Diff. AlphaProof Code là khuôn khổ của Google để viết các đặc tả phần mềm với sự hướng dẫn của con người và tạo ra các bằng chứng đã được kiểm tra bằng các tác nhân AI. Nghiên cứu này nhắm mục tiêu libsignal, thư viện Rust triển khai giao thức nhắn tin của Signal, bên trong một chương trình dòng lệnh cụ thể.

0:45 Google đã công bố công việc này hôm nay. Bài báo của họ nói rằng năm nhà nghiên cứu đã làm việc trong hơn bốn tuần. Các tác nhân đã viết các bằng chứng, trong khi con người dành phần lớn nỗ lực của họ cho các đặc tả. Yêu cầu đã tìm cách trở thành những cuộc họp tốn kém hơn nữa. Đặc tả nói lên những gì chương trình phải làm,

Một yêu cầu trở thành mục tiêu bằng chứng như thế nào?

0:59 những gì kẻ tấn công kiểm soát, và những giả định nào mà đối số cần. Người đánh giá hỏi liệu nó có nắm bắt được bảo mật mà mọi người quan tâm hay không. Một câu trả lời đã được kiểm tra đẹp mắt cho một câu hỏi yếu ớt vẫn để câu hỏi đó nguyên vẹn. Nhóm xây dựng dựa trên nghiên cứu trước đó về bắt tay của Signal và khóa tin nhắn ratchet của nó. Các phân tích chính thức đã nghiên cứu các thiết kế đó. Yêu cầu của Google kết nối các đối số bảo mật của họ với một triển khai đã biên dịch thư viện sản xuất không sửa đổi, nơi thiết kế phải tồn tại khi tiếp xúc với mã thực tế. Giám đốc công nghệ của Signal, Ehren Kret,

1:27 mô tả một sự mở rộng vượt ra ngoài các phạm vi xác minh nhỏ hơn trước đây. Chi tiết triển khai bao gồm tin nhắn không theo thứ tự và các phiên đã lưu trữ cho tin nhắn bị trì hoãn. Phần mềm thực tế giữ lại các biên lai mà sơ đồ thanh lịch của bạn đã vứt đi. Các nhà nghiên cứu biên dịch thư viện Rust không sửa đổi bằng trình biên dịch tiêu chuẩn

Tại sao phải chứng minh nhị phân đã biên dịch?

1:41 thành một tệp thực thi Arm 64 Linux. Các định lý của họ mô tả nhị phân đó bằng cách sử dụng một mô hình hướng dẫn chính thức, kết nối khoảng cách giữa mã nguồn và mã máy được tối ưu hóa. Lỗi trình biên dịch làm hỏng một thuộc tính đã nêu sẽ làm cho định lý của nó sai. Do đó, trình biên dịch rời khỏi cơ sở đáng tin cậy cho nhị phân này. Bạn vẫn tin tưởng mô hình hướng dẫn và trình kiểm tra của Lean. Ranh giới tin cậy đã di chuyển, và nó có một địa chỉ. Khoảng sáu triệu rưỡi dòng bằng chứng đã được kiểm tra dựa trên khoảng hai mươi sáu

2:06 nghìn dòng đặc tả và ngữ nghĩa hướng dẫn đáng tin cậy. Đây là số lượng tạo phẩm. Coi chúng như điểm thông minh giống như xếp hạng nhà phát triển theo kích thước của thư mục node_modules của họ.

Những thuộc tính bảo mật nào đã sống sót qua khoảng cách triển khai?

2:16 Các đối số bao gồm bảo mật và xác thực tin nhắn, với bí mật chuyển tiếp và bảo mật sau khi bị xâm phạm theo các mô hình đã nêu. Hai điều cuối cùng đó mô tả giới hạn về thiệt hại do khóa bị đánh cắp và phục hồi sau khi trao đổi mới. Mỗi đảm bảo có các điều kiện về kẻ tấn công và phiên. Các nguyên tắc mật mã nằm sau các hợp đồng đáng tin cậy. Bằng chứng giả định rằng các thủ tục đó hoạt động như đã chỉ định và dựa vào các giả định bảo mật mật mã. Một bằng chứng lý tưởng hóa mật mã; bằng chứng khác lập luận về xác suất thành công của kẻ tấn công.

2:42 Cả hai đều có những hạn chế về các kịch bản mà chúng bao gồm. Hãy hỏi bản dựng nào, thuộc tính nào và giả định nào. Kết quả này liên quan đến bộ khung dòng lệnh của các nhà nghiên cứu. Tin nhắn nhóm là công việc trong tương lai, và mô hình tính toán loại trừ trạng thái đa thiết bị. Gọi mọi cài đặt Signal là không có lỗi là lạc đề so với định lý. Các nhà nghiên cứu đã tái tạo lại hai lỗi Signal đã được sửa trước đó vào

Đặc tả có thể từ chối mã bị lỗi không?

3:02 các bản sao bị cô lập và biên dịch chúng. Các bằng chứng đã kiểm tra cho thấy các nhị phân đó đã vi phạm định lý bảo mật tượng trưng. Điều đó đã kiểm tra xem liệu đặc tả có thể từ chối các triển khai bị lỗi thực tế hay không. Dấu kiểm màu xanh lá cây của bạn cần một bài kiểm tra màu đỏ. Google công bố các đặc tả và bằng chứng với hướng dẫn kiểm tra. Kho lưu trữ nói rằng một bản dựng sạch mất hàng giờ và bộ nhớ đáng kể. Đọc thông báo dễ dàng hơn đáng kể trên máy tính xách tay. Mô hình phần cứng và các hợp đồng đáng tin cậy vẫn cần xem xét.

3:26 Tôi chưa xây dựng lại tạo phẩm khổng lồ cho tập này. Chúng tôi đang báo cáo kết quả đã công bố và các ranh giới của nó. Người ngoài có một con đường để kiểm tra nó, điều đó quan trọng hơn đối với tôi so với một vòng chiến thắng AI khác. Bây giờ là cái bẫy.

Một bằng chứng đúng có thể trả lời sai câu hỏi không?

3:36 Lean có thể chấp nhận một bằng chứng đúng của một tuyên bố mà hầu như không yêu cầu gì. Các giả định không thể có thể làm cho một định lý trở nên trống rỗng. Thay đổi một định nghĩa được chôn dưới định lý tiêu đề có thể làm suy yếu mục tiêu. Bài báo thiết kế các kiểm tra chống lại điều này. Người gác cổng giữ một đặc tả đã được phê duyệt được giữ lại mà các tác nhân chứng minh không thể ghi vào. Họ có thể đề xuất sửa đổi thông qua một quy trình sửa đổi riêng biệt. Suy yếu bảo mật được leo thang như một lỗi tiềm ẩn. Tuyên bố thành công của người chứng minh không có thẩm quyền ở đây.

4:00 Con người giải quyết các thay đổi đối với các giả định đáng tin cậy, trực tiếp hoặc thông qua chính sách của họ, và xem xét các sửa đổi sau mỗi chiến dịch. Phán đoán của chuyên gia vẫn chịu trách nhiệm. Tác nhân có thể yêu cầu một nhiệm vụ khác. Nó không thể tự cho mình một điểm đậu.

Điều gì nắm bắt các mục tiêu đang thay đổi?

4:13 Đây là kiểm tra đã hứa. Trình so sánh của Lean so sánh định lý và mọi định nghĩa mà nó phụ thuộc vào với bản sao đã được phê duyệt được bảo vệ đó. Nó cũng kiểm tra các tiên đề được phép và phát lại bằng chứng trong một hạt nhân mới. Do đó, việc làm suy yếu một định nghĩa hỗ trợ một cách lặng lẽ sẽ thay đổi thứ đang được so sánh. Một bằng chứng được chấp nhận phải thiết lập mục tiêu đã được phê duyệt. Điều đó vẫn khiến con người chịu trách nhiệm lựa chọn một mục tiêu mạnh mẽ và các giả định trung thực. Đối với quy trình làm việc AI của riêng bạn, hãy giữ các tiêu chí chấp nhận ngoài

4:37 quyền chỉnh sửa của người làm việc và xem xét các thay đổi được đề xuất riêng biệt. Kết quả của Google làm cho sự tách biệt đó trở nên cụ thể. Người viết bằng chứng làm việc; ranh giới kiểm tra quyết định liệu nó có được tính hay không. Nếu bạn muốn đọc điều này hơn là nghe tôi nói, the diff sẽ đến hộp thư đến của bạn mỗi sáng, miễn phí tại thedailydiff.dev, liên kết bên dưới. Vì vậy, phán quyết hôm nay là SHIP IT.

Tôi có nên triển khai quy trình làm việc bằng chứng này không?

4:54 Tôi sẽ triển khai quy trình làm việc bằng chứng đã kiểm tra này vì yêu cầu đã được phê duyệt vẫn tách biệt với tác nhân tạo ra câu trả lời. Tôi sẽ giữ phạm vi và các giả định gắn liền với mọi kết quả. Đăng ký, nhấn chuông, và cho tôi biết trong phần bình luận nếu bạn đã đóng dấu nó khác. Và đó là diff cho ngày hôm nay. Tôi là Niko từ Axrisi. Hợp nhất một cách có trách nhiệm.

Nguồn

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub