Η Google DeepMind σημείωσε ένα ιστορικό ορόσημο στον τομέα της κυβερνοασφάλειας, επιτυγχάνοντας κάτι που μέχρι πρόσφατα θεωρούνταν πρακτικά αδύνατο: απέδειξε μαθηματικά ότι ο εκτελέσιμος κώδικας του πρωτοκόλλου κρυπτογράφησης του Signal πληροί απόλυτα τις βασικές προδιαγραφές ασφαλείας και λειτουργεί χωρίς σφάλματα.
Η εξέλιξη αυτή έχει παγκόσμιο αντίκτυπο, καθώς το πρωτόκολλο του Signal δεν προστατεύει μόνο την ομώνυμη εφαρμογή επικοινωνίας, αλλά αποτελεί τη ραχοκοκαλιά της ιδιωτικότητας για δισεκατομμύρια χρήστες διεθνώς, αφού αφορά υπηρεσίες όπως το WhatsApp και το Google Messages.
Η δυνατότητα της τεχνητής νοημοσύνης να παρέχει την μαθηματική επαλήθευση του λογισμικού μέσα σε μόλις λίγες εβδομάδες ανοίγει τον δρόμο για την άμεση εφαρμογή της μεθόδου σε κρίσιμες υποδομές, όπως τραπεζικά συστήματα, ηλεκτρικά δίκτυα και ιατρικές συσκευές, εξαλείφοντας κρίσιμες ευπάθειες προτού ο κώδικας τεθεί σε παραγωγική λειτουργία.
Πώς επετεύχθη η επαλήθευση: Το σύστημα AlphaProof Code
Το εντυπωσιακό αυτό επίτευγμα κατέστη εφικτό χάρη στο AlphaProof Code, ένα καινοτόμο πλαίσιο πρακτόρων τεχνητής νοημοσύνης που αναπτύχθηκε για τυπική μαθηματική επαλήθευση (formal verification) σε πρωτοφανές βάθος, συνδυάζοντας την εξειδίκευση ανθρώπων ερευνητών με την υπολογιστική ισχύ προηγμένων μοντέλων.
Πρόκειται, όπως αναφέρει η Google, για ένα σημαντικό επίτευγμα και την πρώτη φορά που η τεχνητή νοημοσύνη αξιοποιείται για την πλήρη τυπική επαλήθευση ενός κρυπτογραφικού πρωτοκόλλου ευρείας κλίμακας, το οποίο χρησιμοποιείται καθημερινά σε δισεκατομμύρια συσκευές.
Το AlphaProof Code λειτουργεί ως ένα σύστημα πολλαπλών πρακτόρων μεγάλων γλωσσικών μοντέλων (multi-LLM agentic framework), το οποίο κατανέμει τις επιμέρους εργασίες ακριβώς όπως θα έκανε μια ερευνητική ομάδα. Αρχικά, οι επιστήμονες της Google DeepMind συνεργάστηκαν με τα συστήματα για να μεταφράσουν τις απαιτήσεις ασφαλείας του Signal σε μαθηματικές προδιαγραφές, με ανθρώπους ειδικούς να ελέγχουν κάθε στάδιο.
Στη συνέχεια, πράκτορες που βασίζονται στο μοντέλο Gemini Carbon ανέλαβαν τη σύνταξη των αποδείξεων, παράγοντας περισσότερες από έξι εκατομμύρια γραμμές κώδικα στη γλώσσα Lean.
Ελάχιστη ανθρώπινη παρέμβαση και δοκιμές σε πραγματικά σφάλματα
Κατόπιν, οι πράκτορες αξιολόγησαν τις αποδείξεις και υπέδειξαν στους επιστήμονες μόνο εκείνα τα σημεία που απαιτούσαν ανθρώπινο έλεγχο, τα οποία αντιστοιχούσαν σε μόλις 1% της συνολικής βάσης κώδικα, επιτυγχάνοντας τεράστια εξοικονόμηση χρόνου.
Ενώ οι παραδοσιακές προσπάθειες τυπικής επαλήθευσης σταματούσαν συνήθως σε θεωρητικά μοντέλα, η προσέγγιση της Google DeepMind απέδειξε ότι ο πραγματικός, μεταγλωττισμένος κώδικας διατηρεί απαρέγκλιτα κρίσιμες εγγυήσεις ασφαλείας, όπως η προστασία των μηνυμάτων πριν και μετά από ενδεχόμενη παραβίαση συσκευής (Forward Secrecy και Post-Compromise Security).
Κάπως έτσι, η εταιρεία ολοκλήρωσε σε μόλις τέσσερις εβδομάδες μια διαδικασία που στο παρελθόν θα απαιτούσε χρόνια εντατικής εργασίας από εξειδικευμένες ομάδες. Για να διασταυρώσουν την αξιοπιστία της διαδικασίας και να επιβεβαιώσουν ότι το AlphaProof Code μπορεί να διακρίνει τον ασφαλή από τον ελαττωματικό κώδικα, οι ερευνητές επανέφεραν σκόπιμα δύο γνωστά σφάλματα παλαιότερων εκδόσεων σε απομονωμένο περιβάλλον. Το σύστημα εντόπισε άμεσα τις αδυναμίες, παράγοντας πλήρως επαληθευμένες μαθηματικές αποδείξεις ότι οι συγκεκριμένες εκδόσεις ήταν πράγματι ευάλωτες.
