Τυπική Επαλήθευση Επιβολής Ακεραιότητας Ροής-ελέγχου Με Ετικέτες

Abstract

Μια ευρεία γκάμα επιθέσεων λογισμικού προσπαθούν να ανακτήσουν τονέλεγχο ροής του προγραμμάτος με σκοπό να τροποποιήσουν τησυμπεριφορά του. Η Ακεραιότητα Ελέγχου-Ροής είναι μία αποτελεσματικήπολιτική ασφαλείας, που μπορεί να αποτρέψει όλες τις επιθέσεις πουεπιχειρούν να παρακάμψουν την αρχική ροή ελέγχου του προγράμματος. Σε αυτή τη διπλωματική εργασία, χρησιμοποιούμε το εργαλείοδιαδραστικών αποδείξεων Coq για να αιτιολογήσουμε τυπικά τηνορθότητα και την αποτελεσματικότητα ενός δυναμικού ελεγκτή πουεπιβάλλει Ακεραιότητα Ελέγχου-Ροής, βασιζόμενος σε ένα καινοτόμομηχανισμό ασφαλείας που χρησιμοποιεί λογισμικί και υλικό.Συγκεκριμένα, αποδεικνύομε οτι ο μηχανι-σμός επιβάλλει ΑκεραιότηταΕλέγχου-Ροής ακόμα και υπό την παρουσία ενός ισχυρού κακό-βουλουχρήστη. Επιπλέον αποδεικνύουμε μέσω εκκαθάρισης ότι ένα μηχάνημα στοοποίο τρέχει ο δυναμικός ελεγκτής για την Ακεραιότητα Ελέγχου-Ροής,επακριβώς εξομοιώνει όλες τις συμπεριφορές ενός αφηρημένουμηχανήματος που έχει Ακεραιότητα Ελέγχου-Ροής εκ κατασκευής.