Formal Notions of Non-interference and Liveness for Distributed Systems

The thesis provides a formal framework for liveness and security of distributed systems. It proposes new approaches for defining secure and serviceable systems, and discusses associated model-checking methods. In modeling distributed systems, we assume that components are classified as either 'service provider' or 'user'. The actions performed in the system are either observable by the users or hidden internal actions. A service provider is responsible for providing a reliable service to the users and protection of sensitive information. Regarding the serviceability, the thesis examines distributed systems in which an attacker can try to break down the system and provides a novel notion of liveness called 'observable liveness' which guarantees that the service provider will continue to give the requested services to the users. In the observable liveness setting, we give the control of some observable actions to the user. Intuitively, a distributed system is observably live if, whatever state is reached, a user can force the system to get the requested service by using the controllable actions. This notion is formalized with '1-safe' Petri nets, its properties are studied and it is compared with the classical liveness notion. The thesis also discusses a possible application of infinite games on finite graphs for checking observable liveness. On the security side, the thesis considers information flow and non-interference. It provides several new notions of non-interference for Petri nets, and compares them with notions already proposed in the literature. In the considered setting, the transitions of a Petri net are partitioned into two disjoint sets: the 'low' (observable) and the 'high' (unobservable/hidden) transitions. The attacker knows the structure of the system and tries to deduce information about the high transitions by observing the low transitions. A Petri net is considered 'secure', or 'free from interference', if, from the observation of the occurrence of a low transition, or a set of low transitions, it is not possible to infer information on the occurrence of a high transition. The new non-interference notions rely on net unfolding and on two new relation families among transitions called 'reveals' and 'excludes'. The thesis discusses two methods for checking non-interference. The first method is based on translating the underlying relations, reveals and excludes, into LTL and applying LTL model-checking methods. The second method is based on computing the reveals and the excludes relations on finite prefixes of unfoldings.

La tesi propone una cornice formale per la vivezza e la sicurezza di sistemi distribuiti, e nuovi approcci per definire sistemi sicuri e 'serviceable'. Discute inoltre i relativi metodi di model-checking. Nel modellare sistemi distribuiti, classifichiamo i componenti di un sistema come 'service provider' o 'utenti'. Le azioni che occorrono sono osservabili dagli utenti o interne e nascoste. Un service provider deve garantire agli utenti un servizio affidabile e la protezione delle informazioni riservate. Per quanto riguarda la serviceability, la tesi esamina sistemi distribuiti nei quali un attaccante cerca di interrompere il funzionamento del sistema, e propone una nuova nozione di vivezza, detta 'vivezza osservabile', che garantisce che il server continui a erogare il servizio richiesto agli utenti. In tale contesto supponiamo che l'utente controlli alcune azioni osservabili. Intuitivamente, un sistema distribuito è osservabilmente vivo se da qualunque stato un utente può guidare il sistema, per mezzo delle azioni controllabili, fino a ricevere il servizio richiesto. Questa nozione è formalizzata per mezzo delle reti di Petri '1-safe'; se ne studiano le proprietà, e la si confronta con la nozione tradizionale di vivezza. La tesi discute l'applicazione di giochi infiniti su grafi finiti per verificare la vivezza osservabile. Per quanto riguarda a sicurezza, la tesi considera il flusso di informazione e la non-interferenza. Si danno diverse nuove nozioni di non-interferenza per le reti di Petri, e le si confrontano con quelle presenti nella letteratura. In questo approccio, le transizioni di una rete di Petri sono ripartite in due insiemi: transizioni 'basse' (osservabili) e transizioni 'alte' (nascoste). L'attaccante conosce la struttura del sistema e cerca di dedurre informazioni sulle transizioni alte dall'osservazione delle transizioni basse. Una rete di Petri è 'sicura', o 'libera da interferenza' se non è possibile inferire informazioni sull'occorrenza di una transizione alta, a partire dall'osservazione dell'occorrenza di una o più transizioni basse. Le nuove nozioni di non-interferenza poggiano sull''unfolding' di una rete e su due famiglie di relazioni fra transizioni, dette 'rivela' e 'esclude'. La tesi discute due metodi per verificare la non-interferenza. Il primo si basa sul tradurre in LTL le relazioni rivela e esclude, e sui metodi noti di model-checking per LTL. Il secondo si basa sulla computazione di rivela e esclude in prefissi finiti dell'unfolding