ISAAC. Integrated system application and authorization co-design

The use of formal methods for system design and system property verification is a topic of great interest in those application area where strong security and reliability guarantees are required. Their goal is to proof mathematically that if the system effectively reflects the model used, then the system will possess specific properties of interest. These guarantees are often based on the assumption that, in general, the inputs offered by the users of the system are reliable and legitimate. In other words, during the design phase of the application part of the system, the risk related to malevolent behaviors of the users is often ignored. For these reason, the application part of the system is usually backed up by an authorization part in charge of the access control aspects, i.e. determine and regulate who is allowed to do what within the system. Unfortunately, the commonly followed practice is to overlook the aspects related to authorization security until the end of the design of the application part of the system. This introduces the risk that integrating the two subsystems may be hard, inefficient or even dangerous. Another aspect of the topic is the fact that, often, the formal design of systems is developed in a top-down fashion: starting from a very abstract model of the system, the model gets refined step-by-step, adding an increasing number of details, until a sufficient degree of concreteness is reached. Albeit the literature offers a number of approaches to both the problems of the management of access control and the verification of system properties during the refinement steps, no method was found capable of offering an efficient solution to both problems simultaneously. iii This thesis introduces ISAAC, a theoretical framework for the integrated co-design of the application and authorization parts of a system. ISAAC allows to model a system at any level of abstraction, designing simultaneously the components related to the application and authorization parts, to help verify the absence of circular dependencies among the system interfaces, and to formally verify that the refinements of the model of the system do not introduce inconsistency. Additionally, a case study modeling the functioning of an hospital as a system is presented. The case study focuses on the subsystem related to the management of personal and medical data of the patients, and verifies that the introduction of the possibility for inter-ward consulting is implementable in a correct way, i.e. without invalidating the expected behavior of the system. In conclusion, the original contributions of this work are: - Offering a theoretical methodology for system design capable to include the authorization aspects of access control since the beginning of the design phase of the application part of the system. - Offering a theoretical methodology for the formal verification of the consistency of the refinement steps of a model a system. - Testing ISAAC in a real-world case study, related to the modeling of a subsystem of an hospital system.

L'utilizzo di metodi formali per la progettazione di sistemi e verifica delle loro proprietà è un tema di grande interesse in quegli ambiti applicativi dove sono richieste forti garanzie di sicurezza ed affidabilità. Il loro scopo è quello di dimostrare matematicamente che, qualora il sistema rispecchi il modello utilizzato, esso possiederà determinate proprietà di interesse. Purtroppo però queste garanzie sono legate al funzionamento del sistema supponendo che, in generale, gli ingressi ricevuti dai suoi utenti siano tutti legittimi ed affidabili. In altre parole, solitamente, non viene considerato, durante la progettazione della parte applicativa del sistema, il rischio che gli utenti abbiano comportamenti illegittimi. Per questo motivo, alla parte applicativa di un sistema viene solitamente affiancata una parte di controllo degli accessi, il cui scopo è di determinare e regolare chi può fare cosa all'interno del sistema. Sfortunamente, la pratica spesso seguita è di trascurare gli aspetti di sicurezza, intesa riguardo al comportamento degli utenti e non alle garanzie contro gli incidenti imprevisti, fino a valle della progettazione della parte applicativa del sistema, correndo così il rischio che l'inserimento del sottosistema dedicato al controllo degli accessi sia difficile, inefficace o addirittura dannoso. In aggiunta a questo, spesso la progettazione formale dei sistemi avviene per gradi e raffinamenti successivi: partendo da un modello molto astratto del sistema, si procede via via aggiungendo un numero sempre maggiore di dettagli, fino ad arrivare a un livello di concretezza sufficiente per lo scopo preffissato. Sebbene esistano, in letteratura, molti approcci sia al problema della gestione del controllo degli accessi che alla verifica delle proprietà del sistema attraverso i suoi raffinamenti modellistici, non è stata trovata nessuna metodologia in grado di offrire simultaneamente una soluzione efficace ad entrambi gli aspetti. In questa tesi viene presentata ISAAC, una metodologia teorica di approccio alla progettazione integrata delle parti di applicazione e controllo degli accessi di un sistema. ISAAC consente di modellare rigorosamente un sistema ad un qualsiasi livello di astrazione, progettando congiuntamente sia le componenti legate agli scopi applicativi che quelle legate alla sicurezza, verificare l'assenza di dipendenze circolari tra le interfacce del sistema, e verificare formalmente che eventuali raffinamenti del modello del sistema siano tali da non introdurre inconsistenze. Viene inoltre presentato un caso di studio che modelizza il funzionamento di una parte di una struttura ospedaliera, in particolare quella legata alla gestione dei dati personali e delle terapie dei pazienti, e che verifica che l'introduzione di consulenze mediche tra i vari reparti è realizzabile in modo corretto, cioè senza invalidare il comportamento previsto dal modello di base che non prevede consulenze. In sintesi, i contributi originali sono: - Fornire una metodologia teorica per la progettazione di sistemi che includa gli aspetti di sicurezza del controllo degli accessi fin dall'origine della progettazione della parte applicativa del sistema. - Fornire una metodologia teorica per la verifica formale della consistenza dei passi di raffinamento del modello del sistema. - Testare ISAAC in un caso d'uso del mondo reale, in particolare nella modellizzazione di un sotto-sistema di una struttura ospedaliera.