Please use this identifier to cite or link to this item: http://hdl.handle.net/10889/15435
Title: Ανάπτυξη εφαρμογής κυβερνοφυσικού συστήματος με επιβεβαίωση προδιαγραφών
Other Titles: Development of application of cyberphysical system with specifications verification
Authors: Χατζής, Ιωάννης
Keywords: Πιστοποίηση προδιαγραφών
Ασφάλεια κώδικα
Αυτόματη απόδειξη θεωρημάτων
Βοηθός απόδειξης
Keywords (translated): Specification verification
Code security
Automated theorem proving
Proof assistant
Abstract: Το παρόν διαπραγματεύεται το ζήτημα της αυτοματοποιημένης απόδειξης επαλήθευσης προδιαγραφών για ένα πρόγραμμα ή εφαρμογή με χρήση λογισμικού Coq αυτόματου βοηθού αποδείξεων (δίνοντας μια επισκόπηση της λειτουργικότητας του εργαλείου και της διαδικασίας για το πώς θα επιχειρούσε κανείς μια τέτοια προσπάθεια). Ένα από τα προβλήματα που αντιμετωπίζεται στον σύγχρονο κόσμο με το software είναι ότι ξεφεύγει από τον πιθανό έλεγχο του δημιουργού λόγω μεγέθους και πολυπλοκότητας οδηγόντας στην εισαγωγή λαθών και κενών ασφαλείας που συχνά είναι αδύνατο να προβλεφθούν εκ των προτέρων. Ο τρόπος που θα προτείνουμε εδώ για να διασφαλιστεί η σωστή λειτουργία ενος μέρους κώδικα ώστε να μην μπορεί να χρησιμοποιηθεί για διαφορετικό σκοπό από ότι προορίζεται από τον δημιουργό μέσω των προδιαγραφών, περιλαμβάνει μετάφραση του κώδικα και των προδιαγραφών σε μια γλώσσα μαθηματικών, και με διατύπωση και απόδειξη θεωρημάτων σχετικών και καλά ορισμένων επιτυγχάνεται η επίσημη διατύπωση του προβλήματος και της λύσης του (με παρόμοιο τρόπο όπως κατοχυρώθηκαν μαθηματικές έννοιες δηλ. Επίσημα και κοινώς αποδεκτά) η οποία είναι η σίγουρη διασφάλιση των προδιαγραφών. Κατόπιν το κομμάτι αυτό κώδικα μπορεί να προστίθεται σε μια βάση ασφαλούς κώδικα η οποία μπορεί να είναι αξιόπιστη να μην προκαλέσει προβλήματα ασφάλειας και bugs. Εκτός της ασφάλειας υπάρχουν και άλλες πιθανές εφαρμογές αυτής της πρακτικής όπως η αυτοματοποίηση του testing για κώδικα, ένα μεγάλο και ανιαρό κομμάτι στην διαδικασία παραγωγής προγραμμάτων. Φυσικά, η ικανότητα χειρισμού τέτοιων εργαλείων με οποιονδήποτε χρήσιμο αποτέλεσμα δεν αποκτάται φθηνά και είναι αρκετά εξειδικευμένη, γεγονός που υποδηλώνει ότι για το άμεσο μέλλον μπορεί να προσφερθεί επιλεκτική εφαρμογή αυτού του τύπου ενίσχυσης της αξιοπιστίας του κώδικα.
Abstract (translated): Τhe present thesis is discussing the argument of automated proving of function according to specifications, of a program or application using Coq Automated Proof Assistant software (while giving an overview of the tool’s functionality and process of how one would attempt such an endeavour). One of the problems faced in the modern world with regards to software is that it gets out of the control of its creator(s) due to its size and complexity, leading to the introduction of errors and security vulnerabilities that are often impossible to predict in advance. The approach we will be suggesting here to ensure the proper function of a piece of code so that it can not be used for a purpose other than that intended by the creator, as described through the specifications, includes translation of the code and its specifications into mathematical language, and with the crafting and proving of relevant and well-defined theorems, the formal formulation of the problem and its solution is achieved (in a similar way as mathematical concepts have been established, i.e formally and commonly accepted) which is the guarantee of the specifications. This piece of code can then be added to a secure/trusted code base that can be relied on to not manifest security issues and bugs. In addition to security, there are other possible applications of this practice such as automating code testing, a large and often tedious part of the programming process. Of course, the ability to handle such tools to any effect is still not cheaply acquired and quite niche which suggests that for the foreseeable future a selective application of this type of fortifying the trustworthiness of code can be afforded.
Appears in Collections:Τμήμα Ηλεκτρολ. Μηχαν. και Τεχνολ. Υπολογ. (ΔΕ)

Files in This Item:
File Description SizeFormat 
Nemertes_Chatzis(ele).pdf3.42 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.