Η Anthropic παρουσίασε τα αποτελέσματα πειραμάτων που χρησιμοποίησαν μοντέλα Τεχνητής Νοημοσύνης για την επίσημη επαλήθευση της αξιοπιστίας και της ασφάλειας υφιστάμενων έργων. Κατά τη διάρκεια του πειράματος, χρησιμοποιήθηκαν μοντέλα Τεχνητής Νοημοσύνης για τη δημιουργία μαθηματικών αποδείξεων της απουσίας σφαλμάτων μνήμης για 123 βιβλιοθήκες ανοιχτού κώδικα που δοκιμάστηκαν στην υποδομή OSS Fuzz.
Η επαλήθευση πραγματοποιήθηκε σε επίπεδο μεταγλωττισμένου κώδικα assembly για την αρχιτεκτονική RISC-V. Ο συνολικός όγκος των παραγόμενων δοκιμίων ανήλθε σε περίπου 180 εκατομμύρια γραμμές κώδικα για το σύστημα επαλήθευσης Rocq Prover (περίπου 600 γραμμές ανά δυαδικό αρχείο με 18 εντολές RISC-V). Οι αποδείξεις δημιουργήθηκαν με αυτόματη μετατροπή υπαρχόντων δοκιμών fuzzing σε επίσημες προδιαγραφές, μετά τις οποίες το μοντέλο Claude AI απέδειξε ότι το πρόγραμμα είναι άψογο για οποιαδήποτε δεδομένα εισόδου έως και 64 MB.
Κατά τη διάρκεια της διαδικασίας δημιουργίας δοκιμών, το μοντέλο Τεχνητής Νοημοσύνης (AI) ήταν σε θέση να εντοπίσει και να προετοιμάσει διορθώσεις για εκατοντάδες σφάλματα που προηγουμένως δεν είχαν εντοπιστεί από τις δοκιμές fuzz. Μεταξύ άλλων, αυτά περιελάμβαναν ευπάθειες υπερχείλισης buffer κατά την επεξεργασία ορισμένων δεδομένων εισόδου (π.χ., CVE-2026-56132 στο libexpat), καθώς και λογικά σφάλματα. Επιπλέον, το μοντέλο Τεχνητής Νοημοσύνης (AI) χρησιμοποιήθηκε για να αποδειχθεί η συμμόρφωση της υλοποίησης του αλγορίθμου zlib από τον πυρήνα. Linux Προδιαγραφές RFC 1950.
Ένας διερμηνέας για ένα υποσύνολο της Python δημιουργήθηκε επίσης στο Rust, για τον οποίο προετοιμάστηκε μια επίσημη απόδειξη συμμόρφωσης με τη σημασιολογία του CPython χρησιμοποιώντας το κιτ εργαλείων Verus. Για να συγκριθεί η συμπεριφορά με το CPython, εκτελέστηκαν πάνω από 1.7 εκατομμύρια τυχαία δημιουργημένα προγράμματα Python. Στο 99.95% των περιπτώσεων, τα αποτελέσματα της εκτέλεσης αυτών των προγραμμάτων στη νέα υλοποίηση και στο CPython ταίριαζαν και τυχόν αποκλίσεις που βρέθηκαν ήταν γνωστές περιπτώσεις ακμής.
Η επίσημη επαλήθευση εγγυάται τη συμμόρφωση με τις προδιαγραφές, αλλά δεν εξαλείφει πλήρως τα ζητήματα ασφαλείας, καθώς οι κίνδυνοι που προκαλούνται από προβλήματα πολυνηματοποίησης, δυναμική σύνδεση και ανώμαλη συμπεριφορά σε πραγματικό υλικό παραμένουν ανεπίσημοι. Ένα βασικό πλεονέκτημα της προτεινόμενης προσέγγισης είναι ότι λειτουργεί απευθείας με δυαδικά αρχεία, εξαλείφοντας την ανάγκη επανεγγραφής υπάρχοντος κώδικα σε επίσημα επαληθεύσιμες γλώσσες.
Πηγή: opennet.ru
