Αποδεδειγμένα ασφαλής ανίχνευση εισαγωγής κακόβουλου κώδικα ή δεδομένων στη μνήμη μιας εφαρμογής - Μητρόπουλος, Κωνσταντίνος (Εθνικό Μετσόβιο Πολυτεχνείο. Σχολή Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών. Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών. Εργαστήριο Λογικής και Επιστήμης Υπολογισμών, 2017)
Στην παρούσα διπλωματική εργασία μελετάμε την υλοποίηση της θεωρητικής ασφάλισης της μνήμης μιας εφαρμογής από κάποιον κακόβουλο ο οποίος μπορεί, κάποια δεδομένη χρονική στιγμή, να γράψει σε αυτήν με κάποιο εξωτερικό τρόπο (πχ με ακτινοβολία ή κάνοντας παράνομη χρήση του DMA) αλλά δεν μπορεί να τη διαβάσει. Η ιδέα ανήκει στους Richard Lipton, Rafail Ostrovsky, και Βασίλη Ζήκα (http://drops.dagstuhl.de/opus/volltexte/2016/6311/ [1]). Η προσέγγιση έχει ενδιαφέρον γιατί είναι provably secure, δηλαδή αποδεδειγμένα ασφαλής και δεν βασίζεται σε ευριστικές μεθόδους ή απλές τεχνικές διασφάλισης που ίσως να δουλεύουν στις περισσότερες περιπτώσεις αλλά δεν είναι αποδεδειγμένα ασφαλείς. Γι' αυτόν τον λόγο στοχεύει σε συγκεκριμένο πρόβλημα με συγκεκριμένες παραδοχές (μη δυνατότητα ανάγνωσης), και το λύνει εξ' ολοκλήρου. Η ιδέα είναι να παρεμβάλουμε, ανάμεσα στα χρήσιμα bytes της μνήμης μιας εφαρμογής κομμάτια κλειδιών (keys) καθώς και Message Authentication Codes, για ελέγχους ακεραιότητας. Προϋποθέτουμε μια ασφαλή CPU η οποία πριν λάβει κάτι από τη μνήμη ελέγχει το αντίστοιχο MAC(<χρήσιμα bytes> || <keyshares>) να είναι ορθό, και μετά προχωρά κανονικά. Όταν λάβει από έναν εξωτερικό παίκτη μια πρόκληση (challenge), συνθέτοντας τα κλειδιά των οποίων τα κομμάτια έχουν διασπαρεί στη μνήμη, αποκρυπτογραφεί ορθά το challenge και απαντάει με το plaintext. Ένας επιτιθέμενος αν αλλάξει τη μνήμη είτε θα αλλάξει κάτι που θα ακυρώνει τα MACs (οπότε η ασφαλής CPU θα σταματήσει να εκτελεί ή θα καταστρέψει τα keyshares), είτε θα αλλάξει όλο το block των χρήσιμων bytes+keyshares+MAC, οπότε θα ακυρώσει τα κλειδιά και θα το καταλάβει ο εξωτερικός παίκτης. Στόχος της διπλωματικής είναι να προσεγγίσουμε τον χρόνο που χρειάζεται για να υλοποιηθεί στην πράξη αυτό το σχήμα σε hardware. Υλοποιούμε λοιπόν την προσομοίωση στο userspace ως μια καλή προσέγγιση (του άνω φράγματος του χρόνου), χρησιμοποιώντας κώδικα που κάνει τις ασφαλείς λειτουργίες. Στον μεν κανονικό κώδικα βάζουμε επιπρόσθετα jmps (για την αγνόηση των keyshares και macs) αλλά και verification calls όταν πρέπει να ελεγχθεί ένα MAC, ενώ την υπόλοιπη μνήμη την προσπελαύνουμε με ειδικούς getters και setters (που ελέγχουν τα MAC για την υπόλοιπη μνήμη). Φυσικά, η μνήμη της εφαρμογής δεν είναι όλη “ασφαλής”, αλλά εμείς δεσμεύουμε ένα κομμάτι της το οποίο το καλούμε ασφαλές και εκτελούμε τις προσομοιώσεις εκεί. Τα αριθμητικά αποτελέσματα καταδεικνύουν ότι κοστίζει αρκετά η συχνή επαλήθευση των MACs, και ο ολικός χρόνος είναι μεγάλος. Προτείνουμε όμως καλύτερες (και αρκετά πιο δύσκολες στην υλοποίηση) τεχνικές ακόμα καλύτερης προσέγγισης, αλλά και ιδέες (όπως η χρήση ασφαλούς cache) που μειώνουν πολύ τον επιπρόσθετο χρόνο.