Τα πρωτόκολλα συναίνεσης αποτελούν θεμελιώδη στοιχεία των κατανεμημένων συστημάτων και των τεχνολογιών blockchain. Σφάλματα στην υλοποίησή τους δύνανται να οδηγήσουν σε αλλοίωση δεδομένων και οικονομικές απώλειες.
Ενώ οι προσεγγίσεις που βασίζονται σε Μεγάλα Γλωσσικά Μοντέλα (LLM) παρουσιάζουν προοπτικές στην ανάλυση κώδικα, αντιμετωπίζουν δυσκολίες με βαθιά λογικά σφάλματα σε επίπεδο πρωτοκόλλου. Αυτά τα σφάλματα περιλαμβάνουν πολύπλοκες συμπεριφορές εξαρτώμενες από την κατάσταση, οι οποίες εκτείνονται σε πολλαπλά στάδια εκτέλεσης.
Παρουσιάζεται το Agora, ένα πλαίσιο πολλαπλών παραγόντων με επίγνωση του πεδίου, το οποίο ενσωματώνει δοκιμές βασισμένες σε υποθέσεις με τις δυνατότητες των LLM. Σκοπός του είναι η συστηματική επαλήθευση πρωτοκόλλων. Το Agora χρησιμοποιεί εξειδικευμένους παράγοντες που συνεργάζονται για την εξερεύνηση των χώρων κατάστασης των πρωτοκόλλων. Επιπλέον, συνθέτουν σενάρια επίθεσης αξιοποιώντας περιορισμούς ειδικούς για το πεδίο και επικυρώνουν τα ευρήματα μέσω επαναληπτικής βελτίωσης. Αυτός ο σαφής διαχωρισμός ρόλων επιτρέπει τη συλλογιστική σχετικά με καθολικές αναλλοίωτες ιδιότητες των πρωτοκόλλων, υπερβαίνοντας την ανάλυση κώδικα μεμονωμένων λειτουργιών.
Η αξιολόγηση του Agora πραγματοποιήθηκε σε τέσσερις υλοποιήσεις πρωτοκόλλων συναίνεσης (Raft, EPaxos, HotStuff, BullShark), χρησιμοποιώντας τέσσερα σύγχρονα LLM. Το Agora ανακάλυψε 15 προηγουμένως άγνωστα λογικά σφάλματα σε επίπεδο πρωτοκόλλου, τα οποία παραβιάζουν ιδιότητες ασφαλείας. Αντιθέτως, οι υφιστάμενοι παράγοντες που βασίζονται σε LLM δεν κατάφεραν να εντοπίσουν κανένα τέτοιο λογικό σφάλμα σε επίπεδο πρωτοκόλλου. Τα αποτελέσματα καταδεικνύουν ότι η συνεργασία πολλαπλών παραγόντων με επίγνωση του πεδίου είναι απαραίτητη για τον εντοπισμό βαθιών λογικών σφαλμάτων σε πολύπλοκα πρωτόκολλα.
Πηγή: ARXIV
