Personal computers, information systems, corporate and home networks of either simple or complex configurations and even Critical Infrastructure networks interconnect through the Net. This connectivity defines the need for access control to and protection of the relevant systems, a need which is increasingly pressing especially when compared with isolated systems and networks. Access control rules are described via security policies which vary from simple to complex where assumptions exist regardless of whether they are obvious to users and administrators and quite often with a lot of exceptions. In such an environment the system administrators are expected to deploy, manage, and verify the integrity of what is applied to the equipment compared to the policy itself. The market has responded to the void created by such a need by providing ad-hoc tools that while evolving as time passes tend to prove Greenpsun’s empirical 10th law of software engineering (“Any sufficiently complicated C or FORTRAN program, contains an ad-hoc, informally specified, bug-ridden, slow implementation of half of Common Lisp”). This dissertation aims by using Mathematical Logic tools and PROLOG right from the start to provide for easier deployment, management and verification of security policies that should be in place. Via using this theoretical background powerful tools that can offer solid help to the daily tasks of the system administrator and the security manager are proposed.
Προσωπικοί υπολογιστές, πληροφορικά συστήματα, εταιρικά και οικιακά δίκτυα απλών και πολύπλοκων διαμορφώσεων ακόμα και δίκτυα Κρίσιμων Υποδομών διασυνδέονται στο Δίκτυο. Από την σύνδεσή τους αυτή απορρέει η ανάγκη για κανόνες πρόσβασης και προστασίας των συστημάτων, ανάγκη αυξημένη σε σχέση με αυτόνομα αποκομμένα συστήματα. Οι κανόνες πρόσβασης περιγράφονται από πολιτικές ασφαλείας, οι οποίες περιγράφονται με ποικίλη πολυπλοκότητα, με υποθέσεις που εννοούνται ή όχι και φυσικά με πολλές εξαιρέσεις. Σε αυτό το περιβάλλον οι διαχειριστές θα πρέπει να υλοποιήσουν, συντηρήσουν και να είναι σε θέση να ελέγχουν την ακεραιότητα των εφαρμοζόμενων πολιτικών σε σχέση με τα περιγραφόμενα και όσα περιμένει ο χρήστης από αυτά. Η αγορά έχει απαντήσει στο κενό που υπάρχει μεταξύ της πολιτικής ασφάλειας και της υλοποίησής της στον εξοπλισμό με συστήματα ad-hoc που όπως εξελίσσονται κατά τη διάρκεια του χρόνου τείνουν να επαληθεύουν τον εμπειρικό 10ο κανόνα του Greenspun για το software engineering («Κάθε αρκετά περίπλοκο πρόγραμμα σε C ή FORTRAN περιέχει μια ανεπίσημη, γεμάτη λάθη, αργή υλοποίηση της μισής Common Lisp»). Η μεταπτυχιακή αυτή διατριβή έρχεται να καλύψει αυτό το γεγονός χρησιμοποιώντας Μαθηματική Λογική και τη γλώσσα PROLOG από την αρχή ώστε να είναι ευκολότερη η περιγραφή, η υλοποίηση, η συντήρηση και ο έλεγχος των εφαρμοζόμενων πολιτικών ασφαλείας. Μέσω του θεωρητικού αυτού υπόβαθρου στόχος είναι η δημιουργία ισχυρών εργαλείων που θα προσφέρουν πραγματική βοήθεια στον διαχειριστή και τον υπεύθυνο ασφαλείας στην καθημερινή του εργασία.
