Η Google DeepMind επαλήθευσε μαθηματικά τον κώδικα κρυπτογράφησης του Signal σε τέσσερις εβδομάδες

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

Το πρωτόκολλο του Signal δεν προστατεύει μόνο την ομώνυμη εφαρμογή. Σύμφωνα με το ρεπορτάζ, αφορά και υπηρεσίες όπως το WhatsApp και το Google Messages, με αποτέλεσμα να καλύπτει δισεκατομμύρια χρήστες διεθνώς. Η Google χαρακτηρίζει το επίτευγμα ως την πρώτη φορά που η τεχνητή νοημοσύνη αξιοποιείται για την πλήρη τυπική επαλήθευση ενός κρυπτογραφικού πρωτοκόλλου τόσο ευρείας κλίμακας.

Πώς λειτουργεί το AlphaProof Code

Το AlphaProof Code είναι ένα πλαίσιο πρακτόρων τεχνητής νοημοσύνης που βασίζεται σε πολλαπλά μεγάλα γλωσσικά μοντέλα και έχει σχεδιαστεί για τυπική μαθηματική επαλήθευση (formal verification). Κατανέμει τις εργασίες με τρόπο που θυμίζει ερευνητική ομάδα.

Στο πρώτο στάδιο, επιστήμονες της Google DeepMind συνεργάστηκαν με τα συστήματα για να μετατρέψουν τις απαιτήσεις ασφαλείας του Signal σε μαθηματικές προδιαγραφές, ενώ ειδικοί έλεγχαν κάθε βήμα. Στη συνέχεια, πράκτορες βασισμένοι στο Gemini Carbon συνέταξαν τις αποδείξεις, παράγοντας περισσότερες από έξι εκατομμύρια γραμμές κώδικα στη γλώσσα Lean.

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

Ο πραγματικός κώδικας και η δοκιμή με γνωστά σφάλματα

Σύμφωνα με την περιγραφή της εξέλιξης, οι παραδοσιακές προσπάθειες τυπικής επαλήθευσης περιορίζονταν συχνά σε θεωρητικά μοντέλα. Η προσέγγιση της Google DeepMind αφορούσε τον πραγματικό, μεταγλωττισμένο κώδικα και κατέδειξε ότι διατηρεί κρίσιμες εγγυήσεις ασφαλείας, όπως η προστασία των μηνυμάτων πριν και μετά από ενδεχόμενη παραβίαση συσκευής (Forward Secrecy και Post-Compromise Security).

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

Οι προοπτικές για κρίσιμες υποδομές

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