Το πρωτόκολλο κρυπτογράφησης του Signal προστατεύει μεγάλο όγκο επικοινωνιών, από την ίδια την εφαρμογή ως το Google Messages και το WhatsApp. Ερευνητές της Google DeepMind έδειξαν τώρα με μαθηματική απόδειξη ότι αρκετές από τις βασικές εγγυήσεις του ισχύουν. Το έργο έγινε σε μόλις τέσσερις εβδομάδες, με ένα νέο πλαίσιο AI που ονομάζεται AlphaProof Code, όπως αναφέρει το WIRED.
Η διαδικασία λέγεται τυπική επαλήθευση. Αντί να δοκιμάζουν το λογισμικό και να ελπίζουν ότι δεν ξέφυγε κάτι, οι ειδικοί αποδεικνύουν με μαθηματικά ότι κάνει ακριβώς αυτό που πρέπει. Στην ασφάλεια λογισμικού την θεωρούν από παλιά το ιδανικό. Το πρόβλημα ήταν ο χρόνος: έπρεπε να περιγραφούν οι ιδιότητες που θέλεις να αποδείξεις, να μετατραπούν σε τύπους και μετά να γραφτεί η απόδειξη. Το τελευταίο βήμα είναι αυτό που οι πράκτορες AI, δηλαδή προγράμματα που εκτελούν μόνα τους πολλά διαδοχικά βήματα, μπορούν να συντομεύσουν σημαντικά.
Δεν βρέθηκε νέο λάθος, βρέθηκαν τα παλιά
Στα τμήματα του πρωτοκόλλου που εξετάστηκαν, η ανάλυση δεν ανακάλυψε καμία άγνωστη ευπάθεια. Οι ερευνητές δοκίμασαν όμως το εργαλείο και σε παλιότερες εκδόσεις του Signal, με γνωστά και προ πολλού διορθωμένα προβλήματα. Το AlphaProof Code τα εντόπισε και έδειξε ότι εκείνες οι εκδόσεις δεν μπορούσαν να επαληθευτούν. Η DeepMind δημοσιεύει την προδιαγραφή και την απόδειξη, για να βοηθήσει άλλες προσπάθειες τυπικής επαλήθευσης.
Η δουλειά έχει όρια. Δεν επαληθεύτηκε ολόκληρη η εφαρμογή του Signal για κινητά. Η ομάδα είχε επίσης ένα προβάδισμα, επειδή το Signal Foundation είχε κάνει στο παρελθόν δική του τυπική επαλήθευση σε μικρότερα τμήματα του κώδικα. Ο τεχνικός διευθυντής του Signal, Ehren Kret, λέει ότι η προσέγγιση της DeepMind επιτρέπει «σημαντική επέκταση» και δίνει ακόμη μεγαλύτερη βεβαιότητα για τις εγγυήσεις ιδιωτικότητας.
Ο άνθρωπος μένει στον βρόχο
Κατά τους ερευνητές, η βασική πρόοδος είναι μια διαδικασία συνεργασίας ανθρώπου και AI. Οι πράκτορες συμμετέχουν και διορθώνουν τον εαυτό τους σχεδόν σε κάθε φάση, αλλά σε κρίσιμα σημεία ζητούν γνώμη και έλεγχο από ανθρώπους. «Δεν θέλουμε έναν κόσμο όπου η AI γράφει τους στόχους και γράφει και τις αποδείξεις, δίνοντας στον εαυτό της τεστ που έφτιαξε η ίδια», λέει ο Swarat Chaudhuri της DeepMind. Σύμφωνα με τον ίδιο, υπάρχει μια μέση λύση.
Ο Pushmeet Kohli, επιστημονικός διευθυντής της Google Cloud και αντιπρόεδρος έρευνας της DeepMind, φαντάζεται τράπεζες και άλλες εταιρείες να λένε «μπορώ να αποδείξω αυτές τις ιδιότητες». Ο Chaudhuri παραδέχεται ότι η απόσταση είναι μεγάλη: «υπάρχει πολύς δρόμος μέχρι να το επεκτείνουμε σε όλο το λογισμικό του κόσμου».
Ανοιχτό μένει το κόστος. Η ανάλυση του Signal έγινε δωρεάν, ως ερευνητικό έργο, και η Google αρνήθηκε να πει πόσο στοίχισε. Αρνήθηκε επίσης να σχολιάσει αν σχεδιάζει εμπορικό προϊόν ή υπηρεσία τυπικής επαλήθευσης.
Πηγή: WIRED
