Βελτιώσεις της Εκφραστικότητας και της Ευκολίας Χρήσης του Εργαλείου State Machine Bug Finder

Abstract

Οι υλοποιήσεις των πρωτοκόλλων δικτύου που διατηρούν εσωτερικές καταστάσεις πρέπει να παρακολουθούν την παρουσία, τη σειρά και τον τύπο των μηνυμάτων που ανταλλάσσονται. Τυ- χόν σφάλματα, τα λεγόμενα σφάλματα μηχανής κατάστασης, μπορούν να θέσουν σε κίνδυνο την ασφάλεια. Το SMBugFinder είναι ένα εργαλείο λογισμικού που παρέχει ένα αυτοματοποιημένο πλαίσιο για την ανίχνευση τέτοιων σφαλμάτων σε υλοποιήσεις πρωτοκόλλων δικτύου. Λαμβάνει ως είσοδο ένα μοντέλο μηχανής κατάστασης της υλοποίησης του πρωτοκόλλου υπό εξέταση και έναν κατάλογο προτύπων σφαλμάτων για το πρωτόκολλο, όπου κάθε πρότυπο σφάλματος καθο- ρίζεται κατάλληλα ως πεπερασμένο αυτόματο. Στη συνέχεια, παράγει ακολουθίες που εκθέτουν τα καταχωρημένα σφάλματα στην υλοποίηση που εξετάζεται. Η τρέχουσα αναπαράσταση των προτύπων σφαλμάτων ως πεπερασμένων αυτομάτων πάνω σε ένα απλό αλφάβητο προσφέρει περιορισμένη εκφραστικότητα σε ορισμένες περιπτώσεις, και η μορφή εισόδου που χρησιμοποιείται επί του παρόντος από το SMBugFinder για τη δημιουργία του καταλόγου προτύπων σφαλμάτων δεν είναι πολύ φιλική προς τον χρήστη. Η διπλωματική αυτή εργασία αντιμετωπίζει αυτές τις δύο ελλείψεις επεκτείνοντας τη λειτουρ- γικότητα του εργαλείου σε δύο διαστάσεις. Πρώτον, εισάγουμε μια γραφική διεπαφή χρήστη (GUI) ώστε να διευκολύνουμε το σχεδιασμό και τον καθορισμό των προτύπων σφαλμάτων με διαδραστικό τρόπο. Η διεπαφή προσφέρει μια διαισθητική λειτουργία μεταφοράς και απόθεσης, καθιστά τον σχεδιασμό πιο φυσικό και υποστηρίζει την εξαγωγή σε διάφορες μορφές. Δεύτερον, εισάγουμε μια νέα γλώσσα ειδικού πεδίου (DSL) που συνοδεύει τα μοτίβα σφαλμάτων, επε- κτείνοντας την ευελιξία και την εκφραστικότητά τους, επιτρέποντας τη χρήση δομών υψηλού ε- πιπέδου, όπως σύνολα, συναρτήσεις και κατηγορήματα, καθώς και απαριθμημένους τύπους που αντιπροσωπεύουν παραμέτρους στα μηνύματα.