ETD

Archivio digitale delle tesi discusse presso l'Università di Pisa

Tesi etd-09162016-152055


Tipo di tesi
Tesi di dottorato di ricerca
Autore
MARGHERI, ANDREA
Indirizzo email
margheri.andrea@gmail.com
URN
etd-09162016-152055
Titolo
A Formal Approach to Specification, Analysis and Implementation of Policy-Based Systems
Settore scientifico disciplinare
INF/01
Corso di studi
INFORMATICA
Relatori
tutor Prof. Pugliese, Rosario
Parole chiave
  • Formal Methods
  • SMT
  • Autonomic Computing
  • Policy Languages
  • Access Control
Data inizio appello
16/10/2016
Consultabilità
Completa
Riassunto
The design of modern computing systems largely exploits structured sets of declarative rules called policies. Their principled use permits controlling a wide variety of system aspects and achieving separation of concerns between the managing and functional parts of systems.

These so-called policy-based systems are utilised within different application domains, from network management and autonomic computing to access control and emergency handling. The various policy-based proposals from the literature lack however a comprehensive methodology supporting the whole life-cycle of system development: specification, analysis and implementation. In this thesis we propose formally-defined tool-assisted methodologies for supporting the development of policy-based access control and autonomic computing systems.

We first present FACPL, a formal language that defines a core, yet expressive syntax for the specification of attribute-based access control policies. On the base of its denotational semantics, we devise a constraint-based analysis approach that enables the automatic verification of different properties of interest on policies.

We then present PSCEL, a FACPL-based formal language for the specification of autonomic computing systems. FACPL policies are employed to enforce authorisation controls and context-dependent adaptation strategies. To statically point out the effects of policies on system behaviours, we rely again on a constraint-based analysis approach and reason on progress properties of PSCEL systems.

The implementation of the languages and their analyses provides us some practical software tools. The effectiveness of the proposed solutions is illustrated through real-world case studies from the e-Health and autonomic computing domains.
File