Η επανάσταση της τυπικής επαλήθευσης μέσω τεχνητής νοημοσύνης
Η τυπική επαλήθευση (formal verification) αποτελεί εδώ και δεκαετίες το «Άγιο Δισκοπότηρο» της ασφάλειας λογισμικού, προσφέροντας μαθηματικές εγγυήσεις ότι ο κώδικας είναι απαλλαγμένος από σφάλματα. Ωστόσο, η υψηλή πολυπλοκότητα και ο τεράστιος χρόνος που απαιτούσαν οι ειδικοί (όπως τα 20 ανθρωποέτη για τον πυρήνα του seL4) περιόριζαν την εφαρμογή της μόνο σε κρίσιμα συστήματα αεροναυπηγικής.
Με τη χρήση προηγμένων μοντέλων όπως το Claude, η κατάσταση αυτή αλλάζει ριζικά. Η προσέγγιση επικεντρώνεται στη μετατροπή των παραδοσιακών fuzz tests σε τυπικές προδιαγραφές ορθότητας πάνω σεcompiled RISC-V δυαδικά αρχεία (binaries).
Από τα fuzz tests στις μαθηματικές αποδείξεις
Η μεθοδολογία αξιοποιεί υπάρχοντα test suites από το Google OSS-Fuzz και τα μετατρέπει σε αυστηρές προδιαγραφές που δηλώνουν ότι ένα πρόγραμμα δεν πρόκειται να καταρρεύσει (crash) για οποιαδήποτε είσοδο κάτω των 64 MB.
- Ο πηγαίος κώδικας και τα fuzz tests μεταγλωττίζονται σε εκτελέσιμα RISC-V.
- Σε συνδυασμό με τα επίσημα μοντέλα σημασιολογίας (semantics) για τη Linux CPU και το λειτουργικό σύστημα, παράγεται το spec.
- Το LLM γράφει τις αποδρθώσεις σε Rocq, οι οποίες επαληθεύονται αυτόματα από το Rocq proof checker.
Κατά τη διάρκεια αυτής της διαδικασίας σε 123 βιβλιοθήκες, το Claude κατάφερε όχι μόνο να αποδείξει την απουσία σφαλμάτων αλλά και να εντοπίσει και να διορθώσει bugs που είχαν διαφύγει για χρόνια, παρά τα τρισεκατομμύρια εκτελέσεις δοκιμών.
Αρχιτεκτονική επαναχρησιμοποίησης και αποδοτικότητα
Ένα από τα μεγαλύτερα εμπόδια στην τυπική επαλήθευση ήταν το τεράστιο κόστος σε υπολογιστικούς πόρους και tokens. Τα νέα ευρήματα δείχνουν ότι η επαναχρησιμοποίηση αποδείξεων (proof reuse) μεταξύ παρόμοιων προγραμμάτων μειώνει δραστικά την απαιτούμενη προσπάθεια. Επειδή το μεγαλύτερο μέρος του κώδικα αρχικοποίησης (όπως το C runtime) είναι κοινό, τα agents μπορούν να προσαρμόζουν έτοιμες αποδρθώσεις σε νέα projects, δημιουργώντας ένα ισχυρό οικοσύστημα επαληθευμένου λογισμικού.