Information flow security in web service compositions
Creators: name: Παρδαλίδου, Χριστίνα Ιωάννη
Publisher: name: Aristotle University of Thessaloniki
Year: 2018
Subjects: Ασφαλής ροή πληροφορίας
Μη-παρεμβολή
Σύνθετες υπηρεσίες ιστού
Information flow
Noninterference
Web service composition

description: The information flow in an executable process refers to the transfer of information between the process variables and how this transfer affects important security properties such as data confidentiality and information integrity. The information flow poses challenging problems related to the design and the runtime enforcement of security policies, which are recurring in many different system contexts, as for example web services, Internet of Things etc. This thesis focuses on the design-time specification and verification of Information Integrity policies for web service compositions. In this particular context, instead of manipulating stored data like in most software applications, web services compute requested information from dynamic data available on the web. We are based on a recently proposed theory and tool for the verification of noninterference in component-based systems, as well as on a tool for translating web service compositions written in the BPEL language into a formal component-based model. We extend and adapt the aforementioned tools as appropriate towards the specification and verification of Information Integrity policies based on the decentralized label model that was first proposed by Liskov (2000).
description: Η ασφαλής ροή πληροφορίας σε μια εκτελέσιμη διεργασία αναφέρεται στην μεταφορά της πληροφορίας μέσω των μεταβλητών της και στο πώς επηρεάζονται από αυτήν την μεταφορά σημαντικές ιδιότητες ασφαλείας, όπως η εμπιστευτικότητα και η ακεραιότητα της πληροφορίας. Η ασφαλής ροή πληροφορίας θέτει κάποια σημαντικά προβλήματα που σχετίζονται με τον σχεδιασμό και την εφαρμογή, κατά την εκτέλεση, των πολιτικών ασφαλείας, προβλήματα που επανεμφανίζονται σε διάφορες περιπτώσεις συστημάτων (π.χ υπηρεσίες ιστού, Διαδίκτυο των Αντικειμένων κ.ά). Οι υπηρεσίες ιστού εξάγουν την πληροφορία από δυναμικά παραγόμενα δεδομένα τα οποία είναι διαθέσιμα στον ιστό, σε αντίθεση με τις περισσότερες εφαρμογές λογισμικού όπου η πληροφορία εξάγεται από δεδομένα που είναι ήδη διαθέσιμα και αποθηκευμένα τοπικά. Συνήθως, οι πολιτικές ασφαλείας χρησιμοποιούνται για να προσδιορίσουν τις προδιαγραφές ασφαλείας ενός συστήματος και για να ελέγξουν την πρόσβαση σε εμπιστευτικά δεδομένα και πόρους. Εντούτοις, αν αυτή η προσέγγιση μπορεί να εφαρμοστεί επιτυχημένα για να επιβάλλει τις προδιαγραφές ασφαλείας σε ένα κεντροποιημένο σύστημα, είναι λιγότερο κατάλληλη για να διατυπώσει τις ανάγκες ασφαλείας σε ένα αποκεντρωμένο σύστημα όπως είναι οι σύνθετες υπηρεσίες ιστού. Αυτή η διατριβή εστιάζει στον προσδιορισμό και στην επαλήθευση πολιτικών ασφαλείας που διασφαλίζουν την ακεραιότητα της πληροφορίας σε σύνθετες υπηρεσίες ιστού κατά το στάδιο του σχεδιασμού τους. Για να επιτευχθεί αυτό, βασιστήκαμε στο εργαλείο secBIP που αναπτύχθηκε πρόσφατα και αφορά στην επαλήθευση της μη-παρεμβολής (noninterference) σε συστήματα βασισμένα σε συστατικά και στο εργαλείο που αναπτύχθηκε για την μετάφραση των σύνθετων υπηρεσιών ιστού, που είναι γραμμένες στη γλώσσα BPEL, σε μοντέλα βασισμένα σε συστατικά. Το secBIP περιορίζεται στην επαλήθευση της μη-παρέμβασης στο πλαίσιο της εμπιστευτικότητας και στην ανάλυση μοντέλων που αποτελούνται μόνο από ατομικά συστατικά. Όμως, τα μοντέλα των σύνθετων υπηρεσιών ιστού είναι πιο σύνθετα (π.χ ιεραρχικά μοντέλα). Διαισθητικά, ο ορισμός της μη-παρεμβολής στις σύνθετες υπηρεσίες ιστού εξαρτάται από τον δημόσιο συγχρονισμό μεταξύ των συστατικών τους και στο πόσο ανεξάρτητη είναι η σύνθεση χαμηλού επιπέδου από την συμπεριφορά των συστατικών που ανήκουν στην σύνθεση υψηλού επιπέδου. Βασισμένοι στην παρατήρηση ότι η τυπικά εκφρασμένη εμπιστευτικότητα είναι συμμετρική με την ακεραιότητα της πληροφορίας, επεκτείναμε και προσαρμόσαμε τα προαναφερθέντα εργαλεία έτσι ώστε να μπορούμε να προσδιορίσουμε και να επαληθεύσουμε πολιτικές ασφαλείας που διασφαλίζουν, εκτός από την εμπιστευτικότητα, την ακεραιότητα της πληροφορίας σε σύνθετες υπηρεσίες ιστού και είναι βασισμένες στο αποκεντρωμένο μοντέλο ετικετών, το οποίο προτάθηκε αρχικά από την Liskov (2000).