Software engineering applications of the OTS/CafeOBJ algebraic specification method

Abstract

The scope of this thesis is twofold. The first part is concerned with the verification of the behavior of Mobile Digital Rights Management (DRM) systems using behavioral algebraic specification techniques. The second part discusses a broader range of engineering applications of behavioral algebraic specifications. These include the verification of executable implementations against behavioral specification, reasoning about concurrent systems and safe consumption of mobile code. Digital Rights Management systems are used to protect digital contents by defining finegrained consumption rules in the form of licenses which govern the whole life cycle of the contents. The Open Mobile Alliance (OMA) is a standardization organization responsible for the creation and maintenance of the Mobile DRM system used by the majority of mobile device constructors. The licenses used to express the consumption rules in this system are written in an XML based language called OMA REL. Additionally, as part of the standard, an algorithm responsible for the selection of the appropriate licenses is defined. These two components play a decisive role in the correct functionality of OMA’s mobile DRM system. Formal methods, which are languages with rigorous mathematical semantics and sound tools-methodologies, can be used to define a strict mathematical description of these components which can be used to reason about their properties, analyze their behavior and additionally design new components. One of the most promising branches of formal methods is behavioral algebraic specifications. By defining a new form of satisfiability, behavioral algebraic specification languages can be used to reason about the behavior of systems in a higher abstraction level which may significantly reduce the size of the specification and the cost of the verification effort. This is also advocated by were the authors state that " experiments seem to indicate thatan object-oriented style of specification even of basic data types (such as sets, lists, etc.) may lead to higher simplicity of code and drastic simplification of verification process". CafeOBJ is a new generation executable algebraic specification language which naturally supports the behavioral specification paradigm. The semantics of the language are based on (but are not limited to) Order Sorted Hidden Algebra and Rewriting Logic. Using CafeOBJ, distributed concurrent systems are specified as infinite state abstract machines and reasoning about these systems is conducted using the methodologies of simultaneous induction and co-induction. A very important concern regarding the proper functionality of mobile DRM systems is the ambiguity of the OMA REL language. This ambiguity may result in unexpected results during the execution of the licenses expressed in OMA REL. To address this issue we use the above methodology to provide a formal semantics of OMA REL in CafeOBJ terms. This allows the use of the CafeOBJ rewrite engine to reason about the behavior of licenses written in OMAREL in an automated way. The correct functionality of the algorithm responsible for the selection of licenses is of paramount importance for the safety of the mobile DRM system. We apply the OTS/CafeOBJ method to formally model, specify and verify the above mentioned license choice algorithm. More specifically, we develop the mathematical model of the OMA decision algorithm as an Observational Transition System (OTS), a kind of transition system expressed in an equational CafeOBJ specification style. Finally, we verify that this algorithm fulfills the following minimum safety property: " whenever a license is chosen for a given content, then the license is valid at that specific time". Despite satisfying this minimum safety property this algorithm causes the loss of rights on contents under certain circumstances. By identifying the cases that cause this loss we suggest an algebraic characterization, aswell as an ordering of OMA licenses. These allow us to redesign the algorithm so as to minimize the losses, in a way suitable for the low computational powers of mobile devices. In addition we provide a formal proof that the proposed algorithm fulfills its intent. The proof is conducted using the OTS/CafeOBJ method for verifying in variant properties. After designing the above algorithm the question of obtaining a correct implementation with respect to the specification was raised. The verification of the design and the implementation of critical object oriented systems are two very important but separated tasks. Behavioral algebraic specification techniques provide very good support for reasoning about the design of a system but do not provide any tools for obtaining acompliant implementation. Design by Contract (DbC) is a very strong implementation paradigm for verifying that the implementation satisfies a specification but provides verylimited capabilities for reasoning about the properties of the specification, i.e. the design of the system. In the DbC paradigm each method of a program contains a specification called acontract, in the style of Ho are logic. A plethora of such formal DbC languages have been defined to express contracts for programming languages like Java and C#. Also, several tools have been built to automatically verify that the implementation of the method satisfies its contract. By combining the behavioral algebraic specification techniques with design by contract tools we propose a new software development paradigm in which reasoning about the design of the system is feasible using the tools and methodologies of the former and reasoning about the compliance of the implementation to the specification is achieved through the tools of the later. This new paradigm is supported by a semantic translation from CafeOBJ specifications to Java Modeling Language (JML) specifications, a design by contract language for Java. To demonstrate the applicability and practicality of the framework, some initial case studies are presented. These are not related to the DRM domain, however they are the first stepin evaluating the feasibility of the approach in a broader setting. We also present some arguments about the soundness of the proposed methodology using a mathematical proof for the correctness of the translation. We argue that all models of the JML specification are models of the CafeOBJ specification, i.e. that the JML specification is are finement of the CafeOBJ specification.

Ο σκοπός αυτής της διπλωματικής εργασίας είναι διττός. Το πρώτο μέρος αφορά την επαλήθευση της συμπεριφοράς των συστημάτων Mobile Digital Rights Management (DRM) με τη χρήση τεχνικών συμπεριφορικών αλγεβρικών προδιαγραφών. Το δεύτερο μέρος εξετάζει ένα ευρύτερο φάσμα εφαρμογών των συμπεριφορικών αλγεβρικών προδιαγραφών. Αυτές περιλαμβάνουν την επαλήθευση των εκτελέσιμων υλοποιήσεων έναντι των συμπεριφορικών προδιαγραφών, τη συλλογιστική σχετικά με τα ταυτόχρονα συστήματα και την ασφαλή κατανάλωση κώδικα κινητής τηλεφωνίας. Τα συστήματα διαχείρισης ψηφιακών δικαιωμάτων χρησιμοποιούνται για την προστασία του ψηφιακού περιεχομένου, καθορίζοντας τους κανόνες για την κατανάλωση αδειών που διέπουν ολόκληρο τον κύκλο ζωής του περιεχομένου. Ο Open Mobile Alliance (OMA) είναι ένας οργανισμός τυποποίησης που είναι υπεύθυνος για τη δημιουργία και τη συντήρηση του συστήματος Mobile DRM που χρησιμοποιείται από την πλειοψηφία των κατασκευαστών κινητών συσκευών. Οι άδειες χρήσης που χρησιμοποιούνται για την έκφραση των κανόνων κατανάλωσης σε αυτό το σύστημα είναι γραμμένες σε γλώσσα XML που ονομάζεται OMA REL. Μια πολύ σημαντική ανησυχία σχετικά με την ορθή λειτουργία των κινητών συστημάτων DRM είναι η αμφισημία της γλώσσας OMA REL. Αυτή η ασάφεια μπορεί να οδηγήσει σε μη αναμενόμενα αποτελέσματα κατά την εκτέλεση των αδειών που εκδίδονται στην OMA REL. Για την αντιμετώπιση αυτού του ζητήματος χρησιμοποιούμε την παραπάνω μεθοδολογία για να παρέχουμε μια επίσημη σημασιολογία της OMA REL σε όρους CafeOBJ. Αυτό επιτρέπει τη χρήση της CafeOBJ για να επαληθευθεί αυτομάτως η συμπεριφορά των αδειών που γράφονται στην OMA REL. Η σωστή λειτουργικότητα του αλγορίθμου που είναι υπεύθυνη για την επιλογή των αδειών είναι υψίστης σημασίας για την ασφάλεια του κινητού συστήματος DRM. Εφαρμόζουμε τη μέθοδο OTS/CafeOBJ για να διαμορφώσουμε τυπικά, να καθορίσουμε και να επαληθεύσουμε τον παραπάνω αλγόριθμο επιλογής άδειας χρήσης. Συγκεκριμένα,αναπτύσσουμε το μαθηματικό μοντέλο του αλγορίθμου απόφασης OMA ως Μεταβατικό Σύστημα Παρατήρησης (OTS), ένα είδος μεταβατικού συστήματος που εκφράζεται σε ένα εξειδικευμένο στυλ προδιαγραφών CafeOBJ. Τέλος, επαληθεύσουμε ότι αυτός ο αλγόριθμος πληροί τις ακόλουθες ελάχιστες ιδιότητες ασφαλείας: " κάθε φορά που επιλέγεται μια άδεια χρήσης για ένα δεδομένο περιεχόμενο, τότε η άδεια ισχύει την συγκεκριμένη χρονική στιγμή". Παρά την ικανοποίηση αυτής της ελάχιστης ιδιότητας ασφαλείας, αυτός ο αλγόριθμος προκαλεί την απώλεια δικαιωμάτων επί του περιεχομένου υπό ορισμένες συνθήκες. Με τον προσδιορισμό των περιπτώσεων που προκαλούν αυτή την απώλεια προτείνουμε έναν αλγεβρικό χαρακτηρισμό, καθώς και μια διάταξη των αδειών της ΟΜΑ. Αυτά μας επιτρέπουν να επανασχεδιάσουμε τον αλγόριθμο έτσι ώστε να ελαχιστοποιούμε τις απώλειες, με τρόπο κατάλληλο για τις χαμηλές υπολογιστικές δυνάμεις των κινητών συσκευών. Επιπλέον,παρέχουμε μια επίσημη απόδειξη ότι ο προτεινόμενος αλγόριθμος εκπληρώνει την πρόθεσή του. Η απόδειξη διεξάγεται χρησιμοποιώντας τη μέθοδο OTS/CafeOBJ για την επαλήθευση αναλλοίωτων ιδιοτήτων. Μετά το σχεδιασμό του παραπάνω αλγορίθμου τέθηκε το ζήτημα της απόκτησης ορθής εφαρμογής σε σχέση με τις προδιαγραφές. Η επαλήθευση του σχεδιασμού και της εφαρμογής κρίσιμων αντικειμενοστραφών συστημάτων είναι δύο πολύ σημαντικά αλλά ξεχωριστά καθήκοντα. Συνδυάζοντας τις τεχνικές συμπεριφοριακών αλγεβρικών προδιαγραφών με τα εργαλεία Design by contract προτείνουμε ένα νέο παράδειγμα ανάπτυξης λογισμικού στο οποίο η συλλογιστική για το σχεδιασμό του συστήματος είναι εφικτή χρησιμοποιώντας τα εργαλεία και τις μεθοδολογίες του πρώτου και η συλλογιστική σχετικά με τη συμμόρφωση της εφαρμογής με τις προδιαγραφές επιτυγχάνεται μέσω των εργαλείων του δεύτερου. Αυτή η νέα μεθοδολογία υποστηρίζεται από μια σημασιολογική μετάφραση από τις προδιαγραφές CafeOBJ σε προδιαγραφές γλώσσας Java Modeling Language (JML). Για να καταδειχθεί η δυνατότητα εφαρμογής και η πρακτικότητα της μεθοδολογίας, παρουσιάζονται ορισμένες μελέτες περιπτώσεων. Αυτά δεν σχετίζονται με τον τομέα DRM,ωστόσο είναι τα πρώτο βήμα στην αξιολόγηση της σκοπιμότητας της προσέγγισης σε ευρύτερο πλαίσιο. Παρουσιάζουμε επίσης κάποια επιχειρήματα σχετικά με την αξιοπιστία της προτεινόμενης μεθοδολογίας χρησιμοποιώντας μια μαθηματική απόδειξη για την ορθότητα της μετάφρασης. Υποστηρίζουμε ότι όλα τα μοντέλα της προδιαγραφής JML είναι μοντέλα της προδιαγραφής CafeOBJ, δηλ. ότι η προδιαγραφή JML είναι μια βελτίωση (refinement) της προδιαγραφής CafeOBJ.