AlphaProof Code and Signal: ελεγμένοι έλεγχοι ασφαλείας κώδικα μηχανής και αξιόπιστες υποθέσεις

Τι καλύπτει αυτό το βίντεο

• Οι παράγοντες AI παράγουν υποψήφιες αποδείξεις· ο πυρήνας του Lean ελέγχει αν αυτές τεκμηριώνουν τον εγκεκριμένο από τον άνθρωπο επίσημο ισχυρισμό.
• Ο επαληθευμένος στόχος είναι ένα συγκεκριμένο μεταγλωττισμένο CLI harness της libsignal, με αξιόπιστη σημασιολογία και κρυπτογραφικές συμβάσεις.
• Η απόδειξη του μεταγλωττισμένου δυαδικού αφαιρεί τον μεταγλωττιστή Rust από την αξιόπιστη βάση για τις δηλωμένες ιδιότητες αυτού του δυαδικού.
• Οι ερευνητές αναφέρουν δύο μεμονωμένες επανεισαγωγές προηγουμένως διορθωμένων σφαλμάτων που παραβιάζουν το συμβολικό θεώρημα ασφαλείας τους.
• Ο συγκριτής ελέγχει το θεώρημα και κάθε εξαρτώμενη definηση έναντι μιας προστατευμένης εγκεκριμένης προδιαγραφής· οι τροποποιήσεις περνούν από μια ξεχωριστή αναθεωρημένη διαδικασία.

Μεταφρασμένη μεταγραφή

Μεταφράστηκε από την πρωτότυπη αγγλική αφήγηση. Ο διαθέσιμος ήχος και οι υπότιτλοι ελέγχονται από το YouTube.

Ποιος ελέγχει μια απόδειξη ασφαλείας AI;

0:00 Ένας έλεγχος ασφαλείας AI εξακολουθεί να ακούγεται σαν να εμπιστεύεσαι ένα chatbot. Το νέο αποτέλεσμα της Google για το Signal συνοδεύεται από μαθηματικές αποδείξεις, έναν ξεχωριστό πυρήνα ελέγχει. Σε αυτό το βίντεο, τι απέδειξε η Google; Και πώς σταματούν έναν πράκτορα να μετακινεί τους στόχους; Εδώ είναι η χρήσιμη απάντηση. Τα μοντέλα γράφουν υποψήφιες αποδείξεις, και το Lean ελέγχει τις αποδείξεις έναντι ενός ανθρώπινα εγκεκριμένου ισχυρισμού σχετικά με επιλεγμένο μεταγλωττισμένο κώδικα. Οι άνθρωποι εξακολουθούν να κατέχουν τον ισχυρισμό και τις υποθέσεις.

0:21 Μπορείτε να ελέγξετε το αποτέλεσμα χωρίς να πιστέψετε την ομιλία νίκης του μοντέλου. Ένας ξεχωριστός έλεγχος πιάνει την αθόρυβη αλλαγή της ερώτησης. Θα το ακολουθήσουμε μέχρι τους ορισμούς. Είναι Τρίτη, δέκατη Νοεμβρίου, και αυτό είναι το The Daily Diff. Το AlphaProof Code είναι το πλαίσιο της Google για τη συγγραφή προδιαγραφών λογισμικού με ανθρώπινη καθοδήγηση και τη δημιουργία ελεγμένων αποδείξεων με πράκτορες AI. Αυτή η μελέτη στοχεύει τη libsignal, τη βιβλιοθήκη Rust που υλοποιεί το πρωτόκολλο ανταλλαγής μηνυμάτων του Signal μέσα σε ένα συγκεκριμένο πρόγραμμα γραμμής εντολών.

0:45 Η Google ανακοίνωσε το έργο σήμερα. Η εργασία της αναφέρει ότι πέντε ερευνητές εργάστηκαν για τέσσερις εβδομάδες. Οι πράκτορες έγραψαν τις αποδείξεις, ενώ οι άνθρωποι αφιέρωσαν το μεγαλύτερο μέρος της προσπάθειάς τους στις προδιαγραφές. Οι απαιτήσεις έχουν βρει έναν τρόπο να γίνουν ακόμη πιο ακριβές συναντήσεις. Η προδιαγραφή λέει τι πρέπει να κάνει το πρόγραμμα,

Πώς ένας ισχυρισμός γίνεται στόχος απόδειξης;

0:59 τι ελέγχει ένας εισβολέας, και ποιες υποθέσεις χρειάζεται το επιχείρημα. Οι αναθεωρητές ρωτούν αν αποτυπώνει την ασφάλεια που ενδιαφέρει τους ανθρώπους. Μια όμορφα ελεγμένη απάντηση σε μια αδύναμη ερώτηση αφήνει αυτή την ερώτηση ανέπαφη. Η ομάδα βασίζεται σε προηγούμενη έρευνα για την χειραψία του Signal και το κλειδί μηνυμάτων του ράτσετ. Επίσημες αναλύσεις έχουν ήδη μελετήσει αυτά τα σχέδια. Ο ισχυρισμός της Google συνδέει τα επιχειρήματα ασφαλείας τους με μια μη τροποποιημένη παραγωγή υλοποίηση βιβλιοθήκης, όπου το σχέδιο πρέπει να επιβιώσει της επαφής με πραγματικό κώδικα. Ο Chief Technology Officer του Signal, Ehren Kret,

1:27 περιγράφει μια επέκταση πέρα από τα μικρότερα πεδία προηγούμενης επαλήθευσης. Οι λεπτομέρειες υλοποίησης περιλαμβάνουν μη ταξινομημένα μηνύματα και αρχειοθετημένες συνεδρίες για καθυστερημένα μηνύματα. Το πραγματικό λογισμικό κρατά τις αποδείξεις που πέταξε το κομψό σας διάγραμμα. Οι ερευνητές μεταγλωττίζουν την μη τροποποιημένη βιβλιοθήκη Rust με τον τυπικό

Γιατί να αποδειχθεί το μεταγλωττισμένο δυαδικό;

1:41 μεταγλωττιστή σε ένα εκτελέσιμο Arm 64 Linux. Τα θεωρήματά τους περιγράφουν αυτό το δυαδικό χρησιμοποιώντας ένα επίσημο μοντέλο οδηγιών, φτάνοντας απέναντι στο κενό μεταξύ πηγαίου κώδικα και βελτιστοποιημένου κώδικα μηχανής. Ένα σφάλμα μεταγλωττιστή που παραβιάζει μια δηλωμένη ιδιότητα θα καθιστούσε το θεώρημά του ψευδές. Ο μεταγλωττιστής επομένως αφήνει την αξιόπιστη βάση για αυτό το δυαδικό. Εξακολουθείτε να εμπιστεύεστε το μοντέλο οδηγιών και τον ελεγκτή του Lean. Το όριο εμπιστοσύνης μετακινήθηκε, και έχει μια διεύθυνση. Περίπου έξι και μισό εκατομμύρια γραμμές ελεγμένης απόδειξης βασίζονται σε περίπου είκοσι έξι

2:06 χιλιάδες αξιόπιστες γραμμές προδιαγραφών και σημασιολογίας οδηγιών. Αυτά είναι οι μετρήσεις των τεχνουργημάτων. Η αντιμετώπισή τους ως δείκτες νοημοσύνης είναι σαν την κατάταξη των προγραμματιστών με βάση το μέγεθος του φακέλου modules του node τους.

Ποιες ιδιότητες ασφαλείας επέζησαν του κενού υλοποίησης;

2:16 Τα επιχειρήματα καλύπτουν την εμπιστευτικότητα και την αυθεντικότητα των μηνυμάτων, με forward secrecy και post-compromise security υπό δηλωμένα μοντέλα. Αυτά τα δύο τελευταία περιγράφουν όρια στην απώλεια κλειδιών και την ανάκτηση μετά από νέα ανταλλαγές. Κάθε εγγύηση έχει συνθήκες για τον εισβολέα και τη συνεδρία. Οι κρυπτογραφικές πρωτόγονες βρίσκονται πίσω από αξιόπιστες συμβάσεις. Η απόδειξη υποθέτει ότι αυτές οι ρουτίνες συμπεριφέρονται όπως καθορίζεται και βασίζεται σε κρυπτογραφικές υποθέσεις ασφαλείας. Μια απόδειξη εξιδανικεύει την κρυπτογραφία· η άλλη αναλύει τις πιθανότητες επιτυχίας του εισβολέα.

2:42 Και οι δύο έχουν περιορισμούς στα σενάρια που καλύπτουν. Ρωτήστε ποια έκδοση, ποια ιδιότητα και ποιες υποθέσεις. Αυτό το αποτέλεσμα αφορά το command-line harness των ερευνητών. Η ομαδική ανταλλαγή μηνυμάτων είναι μελλοντική εργασία, και το υπολογιστικό μοντέλο αποκλείει την κατάσταση πολλαπλών συσκευών. Το να χαρακτηρίζουμε κάθε εγκατάσταση του Signal χωρίς σφάλματα βγαίνει εκτός του θεωρήματος. Οι ερευνητές επανεισήγαγαν δύο προηγουμένως διορθωμένα σφάλματα του Signal σε

Μπορεί η προδιαγραφή να απορρίψει τον ελαττωματικό κώδικα;

3:02 απομονωμένα αντίγραφα και τα μεταγλώττισαν. Ελεγμένες αποδείξεις έδειξαν ότι αυτά τα δυαδικά παραβίαζαν το συμβολικό θεώρημα ασφαλείας. Αυτό έλεγξε αν η προδιαγραφή μπορούσε να απορρίψει πραγματικές χαλασμένες υλοποιήσεις. Το πράσινο σας τσεκ χρειάζεται ένα κόκκινο τεστ. Η Google δημοσιεύει τις προδιαγραφές και τις αποδείξεις με οδηγίες ελέγχου. Το αποθετήριο αναφέρει ότι μια καθαρή κατασκευή απαιτεί ώρες και σημαντική μνήμη. Η ανάγνωση της ανακοίνωσης είναι σημαντικά ευκολότερη στον φορητό υπολογιστή. Το μοντέλο υλικού και οι αξιόπιστες συμβάσεις εξακολουθούν να χρήζουν επανεξέτασης.

3:26 Δεν έχω ανακατασκευάσει το τεράστιο τεχνούργημα για αυτό το επεισόδιο. Αναφέρουμε το δημοσιευμένο αποτέλεσμα και τα όριά του. Οι εξωτερικοί παράγοντες έχουν ένα μονοπάτι για να το επιθεωρήσουν, κάτι που με ενδιαφέρει περισσότερο από έναν ακόμη AI γύρο νίκης. Τώρα η παγίδα.

Μπορεί μια σωστή απόδειξη να απαντήσει στη λάθος ερώτηση;

3:36 Το Lean μπορεί να δεχτεί μια σωστή απόδειξη μιας δήλωσης που ζητά σχεδόν τίποτα. Αδύνατες υποθέσεις μπορούν να καταστήσουν ένα θεώρημα κενό. Η αλλαγή ενός ορισμού θαμμένου κάτω από το βασικό θεώρημα μπορεί να αποδυναμώσει το στόχο. Το άρθρο σχεδιάζει ελέγχους έναντι αυτού. Ο φύλακας διατηρεί μια αποθηκευμένη εγκεκριμένη προδιαγραφή στην οποία οι πράκτορες απόδειξης δεν μπορούν να γράψουν. Μπορούν να προτείνουν διορθώσεις μέσω μιας ξεχωριστής διαδικασίας τροποποίησης. Η αποδυνάμωση της ασφάλειας κλιμακώνεται ως πιθανό σφάλμα. Η δήλωση επιτυχίας του αποδεικτικού στοιχείου δεν έχει καμία εξουσία εδώ.

4:00 Οι άνθρωποι κρίνουν τις αλλαγές σε αξιόπιστες υποθέσεις, άμεσα ή μέσω της πολιτικής τους, και επανεξετάζουν τις τροποποιήσεις μετά από κάθε εκστρατεία. Η κρίση των ειδικών παραμένει υπόλογη. Ο πράκτορας μπορεί να ζητήσει διαφορετική ανάθεση. Δεν μπορεί να δώσει στον εαυτό του ένα βαθμό επιτυχίας.

Τι πιάνει τους κινούμενους στόχους;

4:13 Εδώ είναι ο υποσχόμενος έλεγχος. Ο συγκριτής του Lean συγκρίνει το θεώρημα και κάθε ορισμό από τον οποίο εξαρτάται με το προστατευμένο εγκεκριμένο αντίγραφο. Επίσης ελέγχει τα επιτρεπόμενα αξιώματα και επαναλαμβάνει την απόδειξη σε έναν νέο πυρήνα. Η αθόρυβη αποδυνάμωση ενός βοηθητικού ορισμού αλλάζει επομένως το πράγμα που συγκρίνεται. Μια αποδεκτή απόδειξη πρέπει να τεκμηριώσει τον εγκεκριμένο στόχο. Αυτό εξακολουθεί να αφήνει τους ανθρώπους υπεύθυνους για την επιλογή ενός ισχυρού στόχου και έντιμων υποθέσεων. Για τη δική σας ροή εργασίας AI, κρατήστε τα κριτήρια αποδοχής εκτός των

4:37 δικαιωμάτων επεξεργασίας του εργαζομένου και ελέγξτε τις προτεινόμενες αλλαγές ξεχωριστά. Το αποτέλεσμα της Google καθιστά αυτή τη διαχωρισμό συγκεκριμένο. Ο συγγραφέας της απόδειξης κάνει τη δουλειά· το όριο ελέγχου αποφασίζει αν μετράει. Αν προτιμάτε να το διαβάσετε αντί να με ακούσετε να το λέω, το diff φτάνει στα εισερχόμενά σας κάθε πρωί, δωρεάν στο the daily diff dot dev, σύνδεσμος παρακάτω. Έτσι, η σημερινή ετυμηγορία είναι SHIP IT.

Θα έστελνα αυτή τη ροή εργασίας απόδειξης;

4:54 Θα έστελνα αυτή τη ροή εργασίας ελεγμένων αποδείξεων επειδή ο εγκεκριμένος ισχυρισμός παραμένει ξεχωριστός από τον πράκτορα που παράγει την απάντηση. Θα κρατούσα το πεδίο εφαρμογής και τις υποθέσεις συνδεδεμένες σε κάθε αποτέλεσμα. Εγγραφείτε, πατήστε το κουδουνάκι, και πείτε μου στα σχόλια αν θα το είχατε σφραγίσει διαφορετικά. Και αυτή είναι η διαφορά για σήμερα. Είμαι ο Νίκος από την Axrisi. Συγχωνεύστε υπεύθυνα.

Πηγές

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