Παρακαλώ χρησιμοποιήστε αυτό το αναγνωριστικό για να παραπέμψετε ή να δημιουργήσετε σύνδεσμο προς αυτό το τεκμήριο: http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14174
Τίτλος: Υλοποίηση Μιας Γλώσσας Τύπων Με Εφαρμογές Στην Πιστοποίηση Εκτελέσιμου Κώδικα
Συγγραφείς: Μιχάλης Παπακυριάκου
Παπασπύρου Νικόλαος
Λέξεις κλειδιά: συστήματα τύπων
λογισμός των επαγωγικών κατασκευών
προγραμματισμός με αποδείξεις
ασφάλεια εκτελέσιμου κώδικα
ocaml
Ημερομηνία έκδοσης: 25-Οκτ-2004
Περίληψη: Σκοπός της εργασίας είναι η υλοποίηση ενός ελεγκτή τύπων (typechecker) και ενός διερμηνέα (interpreter) για μια γλώσσα τύπων, βασισμένη στο λογισμό των επαγωγικών κατασκευών (Calculus of Inductive Constructions-CIC). Η γλώσσα αυτή είναι αρκετά εκφραστική ώστε να μπορεί ναχρησιμοποιηθεί για την κωδικοποίηση της κατηγορηματικής λογικής υψηλής τάξης. Η υλοποίησή μας μπορεί αφενός να χρησιμεύσει στο πλαίσιο ενός αυτόματου ή ημιαυτόματου συστήματος αποδείξεων θεωρημάτων. Αφετέρου,μπορεί να ενσωματωθεί στο σύστημα τύπων μιας γλώσσας προγραμματισμού ώστε η τελευταία να υποστηρίζει την παραγωγή πιστοποιημένου εκτελέσιμου κώδικα.Η ανάγκη για αξιόπιστο και πιστοποιημένα ασφαλή εκτελέσιμο κώδικα είναι ακόμα μεγαλύτερη σήμερα, από ό,τι στο παρελθόν. Σε πολυάριθμες περιπτώσεις, προβλήματα ασφάλειας και συμβατότητας προγραμμάτων που έγιναν γνωστά, είχαν ως αποτέλεσμα να θέσουν σε κίνδυνο στην λειτουργία μεγάλων συστημάτων και συνεπώς οικονομικές επιπτώσεις στους οργανισμούς που τα χρησιμοποιούσαν. Για την παραγωγή πιστοποιημένου κώδικα μία τεχνική που κερδίζει έδαφος τα τελευταία χρόνια είναι η πιστοποίηση μέσω ισχυρών συστημάτων τύπων που ενσωματώνουν κατάλληλα συστήματα λογικής, μέσω των οποίων διατυπώνονται και αποδεινύονται προτάσεις ασφαλείας.Σε ένα τέτοιο σύστημα πιστοποίησης της ασφάλειας εκτελέσιμου κώδικα, η γλώσσα των τύπων που είναι το θέμα αυτής της εργασίας αποτελεί το τμήμα της γλώσσας προγραμματισμού στο οποίο γίνονται όλοι οι τυπικοί συλλογισμοί. Μια παραλλαγή αυτής της γλώσσας έχει υλοποιηθεί στο εργαλείο υποστήριξης αποδείξεων Coq. Σε ένα πολύγλωσσο προγραμματιστικό περιβάλλον, η γλώσσα των τύπων θα αποτελεί τον κοινό παρονομαστή όλων των γλωσσών προγραμματισμού που μπορούν να χρησιμοποιηθούν για την υλοποίηση συστημάτων. Όμως, η γλώσσα τύπων που υλοποιείται στην παρούσα εργασία είναι χρήσιμη και αυτοτελώς, στο πλαίσιο ενός συστήματος κωδικοποίησης θεωριών και αποδείξεως θεωρημάτων βασισμένου την κατηγορηματική λογική υψηλής τάξης.Η υλοποίηση της γλώσσας τύπων βασίστηκε σε τεχνικές που βελτιστοποιούν την απόδοση, όπως ο κατακερματισμός (hash-consing), η κωδικοποίηση με ανώνυμες μεταβλητές μέσω των δεικτών de-Bruijn και η χρήση της ασθενούς κανονικής μορφής κεφαλής (weak head normal form) για την βελτίωση τηςαπόδοσης του ελέγχου τύπων. Με κριτήριο την απόδοση και τηνλειτουργικότητα που προσφέρει επιλέχθηκε επίσης η γλώσσα υλοποίησης. Χρησιμοποιήθηκε η OCaml, μία γλώσσα που αναπτύχθηκε με τέτοιου είδους χαρακτηριστικά ώστε να προσφέρεται για την ανάπτυξη τέτοιων εφαρμογών. Από τα αποτελέσματα που παρατηρήθηκαν, ελέγχθηκε η ορθότητα καιμετρήθηκε η απόδοση της παρούσας υλοποίησης της γλώσσας τύπων.
URI: http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/14174
Εμφανίζεται στις συλλογές:Διπλωματικές Εργασίες - Theses

Αρχεία σε αυτό το τεκμήριο:
Αρχείο ΜέγεθοςΜορφότυπος 
DT2004-0218.pdf796.07 kBAdobe PDFΕμφάνιση/Άνοιγμα


Όλα τα τεκμήρια του δικτυακού τόπου προστατεύονται από πνευματικά δικαιώματα.