Η Anthropic λέει ότι ο Claude απέδειξε ιδιότητες ασφάλειας σε 123 βιβλιοθήκες

Στις 22 Οκτωβρίου 2026, η Anthropic δημοσίευσε έρευνα, αναφέροντας ότι ο Claude παρήγαγε τυπικές αποδείξεις, ελεγμένες από μηχανή, για ιδιότητες ασφάλειας σε επίπεδο κώδικα assembly RISC-V, για 239 σημεία εισόδου δοκιμών fuzzing σε 123 βιβλιοθήκες ανοιχτού κώδικα, σε συνεργασία με την Theorem.

Σύμφωνα με την Anthropic, ο Claude διόρθωσε τα σφάλματα που εντόπισε και στη συνέχεια απέδειξε ότι τα προγράμματα θα τερματίζονται πάντα κανονικά, χωρίς να προκαλούν σφάλματα ασφάλειας μνήμης ή αποτυχίες ελέγχων assert, για κάθε είσοδο μικρότερη από 64 MB και κάθε μοντελοποιημένη απόκριση του λειτουργικού συστήματος Linux και διάταξη μνήμης. Οι αποδείξεις προϋποθέτουν ότι το πρόγραμμα εκτελείται ως στατικό δυαδικό αρχείο ενός νήματος, με σταθερό όριο μνήμης, σε επεξεργαστή RISC-V που χρησιμοποιεί Linux. Η Anthropic ανέφερε ότι οι αποδείξεις αποτελούνται από περίπου 180 εκατομμύρια γραμμές κώδικα Rocq, ενώ μια τυπική απόδειξη περιλαμβάνει περίπου 600.000 γραμμές και καλύπτει δυαδικά αρχεία με διάμεσο μήκος 18.000 εντολών RISC-V. Η εταιρεία δήλωσε ότι, απ’ όσο γνωρίζει, πρόκειται για την πρώτη μεγάλης κλίμακας προσπάθεια αξιοποίησης της τεχνητής νοημοσύνης για την εφαρμογή τυπικής επαλήθευσης σε λογισμικό παραγωγής, σε επίπεδο κώδικα assembly.

Ένα υποσύνολο των αποδείξεων, μαζί με τη σημασιολογία του RISC-V και του λειτουργικού συστήματος που τις υποστηρίζει, δημοσιεύεται στο GitHub. Η Anthropic ανέφερε ότι δημοσιεύει επίσης τα έμπιστα στοιχεία που δημιουργήθηκαν για το έργο και δεν ήταν ήδη διαθέσιμα στο κοινό, πλήρεις αποδείξεις για δοκιμές fuzzing που δεν χρειάστηκαν διορθώσεις, καθώς και προδιαγραφές για δοκιμές fuzzing τις οποίες δεν κατάφερε να αποδείξει, ενώ δεν δημοσιεύει αποδείξεις που θα μπορούσαν να αποκαλύψουν κάποιο σφάλμα που δεν έχει διορθωθεί.

Μετατροπή δοκιμών fuzzing σε τυπικές αποδείξεις

Η προσέγγιση μετατρέπει την ήδη υπάρχουσα, μεταγλωττίσιμη δοκιμή fuzzing κάθε βιβλιοθήκης σε τυπική προδιαγραφή που κωδικοποιεί έναν κανόνα: η δοκιμή δεν καταρρέει ποτέ για καμία είσοδο μικρότερη από 64 MB. Η προδιαγραφή ορίζεται πάνω στις μεταγλωττισμένες εντολές RISC-V, με τη χρήση της τυπικής σημασιολογίας της Theorem για το σύνολο εντολών RISC-V και τις διεργασίες Linux, ενώ ο ελεγκτής αποδείξεων Rocq επαληθεύει κάθε ολοκληρωμένη απόδειξη βάσει της προδιαγραφής. Η Anthropic λέει ότι έτσι οι προγραμματιστές χρειάζεται να εμπιστεύονται μόνο τρία στοιχεία: τα τυπικά μοντέλα του RISC-V και των διεργασιών Linux, τις ακριβείς διατυπώσεις των θεωρημάτων και τον ίδιο τον ελεγκτή Rocq.

Η Anthropic ανέφερε ότι εφάρμοσε αυτή τη διαδικασία σε εκατοντάδες έργα της πρωτοβουλίας OSS-Fuzz της Google, η οποία παρέχει συνεχή δοκιμή fuzzing για επιλέξιμα έργα ανοιχτού κώδικα και προσθέτει αυτόματα όργανα στα προγράμματα C και C++ μέσω του AddressSanitizer, ενός εργαλείου που προκαλεί κατάρρευση του προγράμματος κάθε φορά που γίνεται ακατάλληλη πρόσβαση στη μνήμη. Παράρτημα με ημερομηνία 22 Οκτωβρίου 2026 περιγράφει αναλυτικά το πλήρες θεώρημα που αποδείχθηκε: για όλες τις εισόδους μικρότερες από 64 MiB και όλες τις διατάξεις μνήμης, ούτε το δυαδικό αρχείο με τα όργανα του ASan ούτε το απλό δυαδικό αρχείο παρουσιάζει σφάλμα, διακόπτεται απότομα ή εμφανίζει μη μοντελοποιημένη συμπεριφορά, ενώ και τα δύο παράγουν πανομοιότυπα ίχνη ανάγνωσης και εγγραφής, συμπεριφορά τερματισμού και τελική κατάσταση του συστήματος αρχείων.

Το παράρτημα αναφέρει ότι ο Claude έγραψε περίπου ένα δισεκατομμύριο γραμμές κώδικα Rocq στη διάρκεια της προσπάθειας, εκ των οποίων περίπου 180 εκατομμύρια γραμμές πέρασαν τον έλεγχο αποδείξεων. Το σημείο εισόδου του αναλυτή cJSON, μήκους 391 γραμμών, συνοδεύτηκε από απόδειξη 630.000 γραμμών, ενώ η fftw3, με 51.000 γραμμές συνδεδεμένες στο δυαδικό αρχείο, συνοδεύτηκε από απόδειξη 480.000 γραμμών. Επειδή επιτρεπόταν στον Claude να διορθώνει τον κώδικα πριν ολοκληρώσει μια απόδειξη, η Anthropic ανέφερε ότι επέβαλε ποινές για τις διορθώσεις, έδινε επιπλέον επιβράβευση για την απόδειξη του ποιες εισόδους άλλαζε κάθε διόρθωση και κατέγραφε και έλεγχε τις διορθώσεις, ώστε να αποθαρρύνει την εκμετάλλευση του μηχανισμού ανταμοιβής.

Σφάλματα που εντοπίστηκαν κατά τις προσπάθειες απόδειξης

Η Anthropic αναφέρει ότι οι προσπάθειες απόδειξης αποκάλυψαν εκατοντάδες σφάλματα, πολλά από τα οποία ήταν απίθανο να εντοπιστούν από ένα εργαλείο fuzzing. Κατά την απόδειξη του σημείου εισόδου μιας βιβλιοθήκης, ο Claude εντόπισε υποχείλιση μετρητή σε έναν αποσυμπιεστή, η οποία προκαλούσε εγγραφή εκτός ορίων, αλλά μόνο με εισόδους περίπου 20 MB που είχαν μία σπάνια, συγκεκριμένη διάταξη. Άλλα ευρήματα περιλάμβαναν ανάγνωση εκτός ορίων σε αποκωδικοποιητή εικόνας, η οποία απαιτούσε είσοδο 64 MB και περισσότερα από 2 GB μνήμης· ανάγνωση εκτός ορίων που απαιτούσε συγκεκριμένη ακολουθία κλήσεων μέσω δύο λαβών προς το ίδιο αρχείο· και τον εκ νέου εντοπισμό του CVE-2026-56132 στο libexpat, το οποίο απαιτούσε βαθιά εμφωλευμένη είσοδο.

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

Πρόσθετα πειράματα και ευρήματα αποδοτικότητας

Πέρα από το OSS-Fuzz, η Anthropic ζήτησε από τον Claude να συντάξει τυπική προδιαγραφή του RFC 1950, του τεχνικού εγγράφου που ορίζει τη μορφή συμπίεσης zlib, και στη συνέχεια να αποδείξει ότι η υλοποίηση zlib του πυρήνα Linux την εφαρμόζει σωστά. Ο Claude απέδειξε απευθείας το δυαδικό αρχείο που είχε μεταγλωττιστεί για x86, χρησιμοποιώντας τυπική σημασιολογία του συνόλου εντολών x86, την οποία είχε δημιουργήσει ο ίδιος. Η Anthropic ανέφερε ότι επανέλαβε τη διαδικασία για έξι ακόμη ευρέως χρησιμοποιούμενες βιβλιοθήκες, εντοπίζοντας μικρά σφάλματα σε ακραίες περιπτώσεις, τα οποία δεν μπορούν να αποτελέσουν αντικείμενο εκμετάλλευσης και υποβάλλονται στα αντίστοιχα upstream έργα. Η εταιρεία ανέφερε επίσης ότι η δημιουργία της σημασιολογίας x86 εντόπισε εκατοντάδες λάθη στην επίσημη τεκμηρίωση αναφοράς και μικρότερο αριθμό σφαλμάτων στο ίδιο το υλικό, καθώς και ότι η εκτέλεση βήμα προς βήμα μέσω της σημασιολογίας μπορεί να εκκινήσει ένα περιβάλλον χρήστη του Ubuntu σε έναν πυρήνα Linux.

Σε ένα άλλο πείραμα, ο Claude δημιούργησε σε Rust έναν διερμηνευτή για ένα μεγάλο υποσύνολο της Python και απέδειξε, χρησιμοποιώντας το εργαλείο επαλήθευσης Verus, ότι συμμορφώνεται με τη σημασιολογία της CPython, όπως αυτή περιγράφεται σε ακαδημαϊκή εργασία. Το τεχνικό παράρτημα αναφέρει ότι αποδείχθηκε η ορθότητα και των 17 επιπέδων του διερμηνευτή, με το θεώρημα να ισχύει ότι «Όποτε ο διερμηνευτής επιστρέφει ένα αποτέλεσμα, αυτό είναι το αποτέλεσμα που ορίζει η τυπική σημασιολογία». Η Anthropic ανέφερε ότι οι εμπειρικές δοκιμές σε 1,7 εκατομμύρια τυχαία παραγόμενα προγράμματα Python έδειξαν συμπεριφορά πανομοιότυπη με την CPython στο 99,95% των δοκιμών· από τα επτά σφάλματα που εισήχθησαν σκόπιμα, πέντε δεν εντοπίστηκαν στις τυχαίες δοκιμές, ενώ και τα επτά κατέρριψαν την απόδειξη.

Για να μετρήσει την αποδοτικότητα, η Anthropic δημιούργησε 36 μικρές εργασίες επαλήθευσης, συρρικνώνοντας πραγματικά σημεία εισόδου του OSS-Fuzz. Έτσι προέκυψαν προγράμματα με 283–2.491 εντολές, των οποίων οι είσοδοι περιορίζονταν στα 64 byte, ενώ το AddressSanitizer αντικαταστάθηκε από ένα περιβάλλον εκτέλεσης «mini-ASan» περίπου 100 εντολών. Η Anthropic αναφέρει ότι το Opus 5.5 αποδεικνύει την ορθότητα των μισών εργασιών χρησιμοποιώντας περίπου 40% λιγότερα token από το Opus 5. Η Anthropic αναφέρει επίσης ότι οι πράκτορες που μπορούσαν να αντιγράφουν ο ένας τις αποδείξεις του άλλου σε έναν κοινόχρηστο χώρο εργασίας χρειάστηκαν 17% λιγότερα token από τους πράκτορες που εργάζονταν μόνοι τους, ότι ορισμένοι τα κατάφεραν αφού προηγουμένως είχαν αποτύχει όταν εργάζονταν μόνοι και ότι οι πράκτορες που εργάζονταν μόνοι τους δεν ολοκλήρωσαν δύο από τις αποδείξεις. Η εταιρεία ανέφερε ότι το ίδιο όφελος από την επαναχρησιμοποίηση εμφανίστηκε σε μεγάλη κλίμακα κατά τη διάρκεια της προσπάθειας με το OSS-Fuzz: ομάδες πρακτόρων αντέγραφαν ολοκληρωμένες αποδείξεις και τις προσάρμοζαν, επειδή μεγάλο μέρος κάθε απόδειξης αφορά κοινό κώδικα αρχικοποίησης του περιβάλλοντος εκτέλεσης C και του AddressSanitizer.

Δηλωμένοι περιορισμοί και το πρόγραμμα OSS Verify

Η Anthropic διευκρινίζει ότι οι αποδείξεις δεν σημαίνουν πως οι βιβλιοθήκες δεν περιέχουν σφάλματα: τυχόν σφάλματα που παραμένουν μπορεί να βρίσκονται είτε στα έμπιστα στοιχεία είτε εκτός του πεδίου εφαρμογής των αποδείξεων. Οι αποδείξεις καλύπτουν στατικά δυαδικά αρχεία RISC-V μονού νήματος, συνδεδεμένα με τη musl libc, ενώ οι περισσότεροι χρήστες εκτελούν αυτές τις βιβλιοθήκες σε x86 ή ARM και τις συνδέουν δυναμικά με τη glibc· επιπλέον, το AddressSanitizer δεν εντοπίζει όλα τα σφάλματα ασφάλειας μνήμης. Η εταιρεία ανέφερε ότι αναμένει πως οι περιορισμοί αυτοί θα καταστούν αντιμετωπίσιμοι καθώς βελτιώνονται τα μοντέλα.

Η Theorem προσφέρει δωρεάν την ίδια διαδικασία σε επιλέξιμα έργα ανοιχτού κώδικα μέσω του προγράμματός της OSS Verify. Η ένταξη γίνεται με αίτημα ενσωμάτωσης που προσθέτει τα αρχεία project.yaml, Dockerfile και build.sh στο αποθετήριο του προγράμματος. Η Theorem αναφέρει ότι αξιολογεί τα έργα με κριτήρια παρόμοια με εκείνα του OSS-Fuzz, δίνοντας προτεραιότητα σε ευρέως χρησιμοποιούμενες κρίσιμες υποδομές. Σύμφωνα με τη Theorem, οι συντηρητές λαμβάνουν μια απόδειξη Rocq, ελεγμένη από τον πυρήνα του Rocq, ότι κανένας στόχος fuzzing δεν καταρρέει με οποιαδήποτε είσοδο έως και 64 MiB· τα σφάλματα που εντοπίζονται κατά τη διαδικασία απόδειξης γνωστοποιούνται ιδιωτικά στους συντηρητές μέσω ηλεκτρονικού ταχυδρομείου, χωρίς προθεσμία δημοσιοποίησης, ενώ η παραγωγή των αποδείξεων μπορεί να διαρκέσει αρκετές ημέρες. Ο οδικός χάρτης της Theorem προβλέπει την επαλήθευση ολόκληρου του οικοσυστήματος Nix, συμπεριλαμβανομένων κρίσιμων υποδομών όπως οι glibc, OpenSSL και cURL.