Η Google DeepMind χρησιμοποιεί πράκτορες ΤΝ για να επαληθεύσει τον βασικό κώδικα μηχανής του Signal

Η Google DeepMind παρουσίασε το AlphaProof Code στις 10 Νοεμβρίου 2026, χρησιμοποιώντας ομάδες πρακτόρων ΤΝ για την παραγωγή αποδείξεων Lean, ελεγμένων από μηχανή, σχετικά με καθορισμένες ιδιότητες ασφάλειας του μεταγλωττισμένου κώδικα libsignal του Signal. Η πενταμελής ερευνητική ομάδα ολοκλήρωσε τις εργασίες απόδειξης σε τέσσερις εβδομάδες και δημοσίευσε τις προδιαγραφές και τα τεκμήρια επαλήθευσης για έλεγχο από τρίτους.

Η εργασία ξεπέρασε το επίπεδο ενός αφηρημένου μοντέλου του σχεδιασμού πρωτοκόλλου του Signal και έφτασε στην ίδια τη μεταγλωττισμένη υλοποίησή του. Οι ερευνητές ενσωμάτωσαν τα μη τροποποιημένα crates libsignal v0.105.4 και SPQR v1.6.0 σε ένα μικρό εργαλείο γραμμής εντολών και στη συνέχεια χρησιμοποίησαν το τυπικό rustc για να δημιουργήσουν ένα στατικά συνδεδεμένο εκτελέσιμο για AArch64 Linux. Η τεχνική εργασία περιγράφει το αποτέλεσμα ως τις πρώτες αποδείξεις ασφάλειας σε επίπεδο πρωτοκόλλου για τον μη τροποποιημένο κώδικα μιας ευρέως χρησιμοποιούμενης υλοποίησης κρυπτογραφικού πρωτοκόλλου.

Πώς το AlphaProof Code κατένειμε την εργασία

Πέντε ερευνητές αφιέρωσαν τέσσερις εβδομάδες στις εργασίες απόδειξης, εκτελώντας συνεχώς πράκτορες στους σταθμούς εργασίας τους και επιδιώκοντας παράλληλα συμβολικές και υπολογιστικές αποδείξεις. Σύμφωνα με την εργασία, οι πράκτορες παρήγαγαν περίπου 6,5 εκατομμύρια γραμμές κώδικα αποδείξεων Lean, ελεγμένου από μηχανή, οι οποίες βασίζονταν σε περίπου 26.000 γραμμές έμπιστων προδιαγραφών και σημασιολογίας AArch64.

Οι άνθρωποι επέλεγαν τις ιδιότητες, επέλυαν ασάφειες και ζητήματα συμβιβασμού στην ασφάλεια, εξέταζαν τις προδιαγραφές και διατηρούσαν την τελική έγκριση. Πράκτορες με την υποστήριξη των Gemini 4 Carbon και Claude Opus 5.5 συνέτασσαν και εξέταζαν αυτές τις προδιαγραφές, με την εξέταση να περιλαμβάνει και μοντέλο διαφορετικής οικογένειας. Στη συνέχεια, ομάδες πρακτόρων του Gemini 4 Carbon παρήγαγαν όλο τον κώδικα των αποδείξεων· κανένας από τους συγγραφείς δεν έγραψε κώδικα αποδείξεων. Οι συνήθεις εκστρατείες χρησιμοποιούσαν 40 έως 80 πράκτορες σε ένα μηχάνημα επί 24 έως 72 ώρες, με έναν συντονιστή και επικεφαλής ομάδων να συντονίζουν τους πράκτορες που εργάζονταν στις αποδείξεις, ενώ οι ρόλοι αρχιτέκτονα και ενοποιητή διατηρούσαν την κοινή βάση αποδείξεων.

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

Κάλυψη της ασφάλειας και δοκιμές με ιστορικά σφάλματα

Στόχος της επαλήθευσης ήταν ο κώδικας συνεδριών ένας προς έναν, που καλύπτει τη χειραψία PQXDH και την ανταλλαγή μηνυμάτων Triple Ratchet. Οι ερευνητές αναφέρουν δύο ανεξάρτητα επιχειρήματα: δέκα συμβολικά θεωρήματα υπό εξιδανικευμένες κρυπτογραφικές παραδοχές και μία υπολογιστική απόδειξη που θέτει όριο στο πλεονέκτημα ενός επιτιθέμενου μέσω κρυπτογραφικών παραδοχών και στατιστικών όρων. Οι ιδιότητες περιλαμβάνουν την εμπρόσθια μυστικότητα, η οποία προστατεύει τα παλαιότερα μηνύματα μετά την κλοπή της τρέχουσας κατάστασης· τον έλεγχο ταυτότητας· την ασφάλεια μετά από παραβίαση, η οποία αφορά την ανάκαμψη μετά από παραβίαση· και τη μυστικότητα της χειραψίας. Το συμβολικό επιχείρημα καλύπτει επιπλέον τη μυστικότητα της χειραψίας μετά από μεταγενέστερη παραβίαση του Diffie–Hellman.

Για να ελέγξει αν αυτές οι προδιαγραφές μπορούσαν να εντοπίσουν πραγματικά σφάλματα, η ομάδα αναίρεσε τις διορθώσεις για δύο σφάλματα του libsignal που είχαν επιδιορθωθεί στο παρελθόν, γνωστά ως «αδύναμη κατάσταση» και «μικρή υποομάδα», και μετέφρασε ξανά τα τροποποιημένα δυαδικά αρχεία. Και στις δύο περιπτώσεις, παρήγαγε αποδείξεις Lean ότι το συμβολικό θεώρημα ασφάλειας δεν ίσχυε. Το δημόσιο αποθετήριο επαλήθευσης διαχωρίζει το υπολογιστικό, το συμβολικό, το κοινό υλικό δυαδικών αρχείων και το υλικό σημασιολογίας AArch64, ενώ τεκμηριώνει τον τρόπο αναδημιουργίας και ανεξάρτητου ελέγχου των αποδείξεων.

Ο Ehren Kret, διευθυντής τεχνολογίας του Signal, δήλωσε ότι η εργασία «μας κάνει να εμπιστευόμαστε ακόμη περισσότερο τις εγγυήσεις απορρήτου του κώδικά μας».

Περιορισμοί και επόμενα βήματα

Οι εγγυήσεις απέχουν πολύ από την πιστοποίηση των πλήρων εφαρμογών του Signal. Αφορούν την έκδοση του libsignal-cli που δημιούργησαν οι ερευνητές και εκτελείται ως νέα διεργασία· η δημιουργία κλειδιών δεν επαληθεύτηκε, η ανταλλαγή μηνυμάτων σε ομάδες αφέθηκε για μελλοντική εργασία, ενώ τα πλευρικά κανάλια και η κατάσταση πολλαπλών συσκευών βρίσκονται εκτός του εξεταζόμενου σεναρίου. Τα κρυπτογραφικά πρωτογενή στοιχεία χαμηλού επιπέδου και επιλεγμένες ρουτίνες εξόδου και βιβλιοθηκών αναπαρίστανται μέσω έμπιστων συμβολαίων. Επομένως, το αποτέλεσμα εξαρτάται επίσης από αυτά τα συμβόλαια, τις εγκεκριμένες προδιαγραφές, τον πυρήνα του Lean, τη σημασιολογία AArch64 και τις παραδοχές σχετικά με τα πρωτογενή στοιχεία.

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

Τα επόμενα βήματα που αναφέρουν οι ερευνητές είναι να ενισχύσουν τα θεωρήματα, να περιορίσουν τη βάση εμπιστοσύνης επαληθεύοντας περισσότερες συνδεδεμένες ρουτίνες και συνδέοντας τα κρυπτογραφικά συμβόλαια με επαληθευμένες υλοποιήσεις, καθώς και να διευρύνουν την κάλυψη ώστε να περιλαμβάνει την ανταλλαγή μηνυμάτων σε ομάδες, τον αποστολέα με απόκρυψη και τα πρωτόκολλα από την πλευρά του διακομιστή. Στόχος τους είναι να επαληθεύουν τις νέες εκδόσεις του libsignal πριν από την κυκλοφορία τους· πρόκειται για ερευνητικό στόχο και όχι για ανακοινωμένη ανάπτυξη.

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