Formal Methods for Wireless Systems

I sistemi wireless sono costituiti da dispositivi che comunicano tra loro per mezzo di un canale radio. Questo paradigma di rete presenta molti vantaggi, ma la presenza del canale radio lo rende intrinsecamente vulnerabile. Di conseguenza, in tale ambito la sicurezza rappresenta un tema importante. I meccanismi di sicurezza messi a punto per i sistemi cablati presentano molti limiti quando vengono utilizzati in una rete wireless. I problemi principali derivano dal fatto che essi operano in modo centralizzato e sotto l'ipotesi di un “mondo chiuso”. Pertanto tecniche formali sono necessarie per stabilire una connessione matematicamente rigorosa tra la modellazione e gli obiettivi di sicurezza. Nella presente tesi si applica il formalismo ben noto del "process calculus" per modellare le principali caratteristiche della comunicazione wireless. Il contributo scientifico è essenzialmente teorico. Verrà proposto un primo process calculus per modellare il passaggio del tempo nei sistemi wireless. Verranno dimostrate alcune interessanti proprietà relative al tempo. Inoltre verrà presentata una rigorosa trattazione dei problemi di collisione. Verranno fornite anche “equivalenze comportamentali” (behavioural equivalence) e verranno dimostrate una serie di leggi algebriche. L'usabilità del calcolo verrà mostrata modellando il Carrier Sense Multiple Access, un diffuso protocollo di livello MAC in cui un dispositivo ascolta il canale prima di trasmettere. Verranno poi analizzati alcuni aspetti di sicurezza, in particolare verrà proposto un modello di trust per le reti ad hoc mobili. Tali reti sono costituite da nodi mobili che comunicano senza l’ausilio di altre infrastrutture. Le reti di tale calcolo verranno modellate come sistemi multilivello perché le relazioni di trust associano ai nodi livelli di sicurezza in base al loro comportamento. Tale modello di trust verrà incluso in un process calculus per reti ad hoc che sarà dotato di equivalenze comportamentali a partire dalle quali verrà sviluppata una "teoria osservazionale" (observational theory). Saranno garantiti sia alcune interessanti proprietà relative alla sicurezza, come la safety in presenza di nodi compromessi, sia risultati di non interferenza. Tale calcolo verrà utilizzato per analizzare una versione “sicura” di un algoritmo per il leader election nelle reti ad hoc. Verrà fornita anche una codifica del protocollo di routing per reti ad hoc chiamato endairA. Infine, il calcolo sul trust verrà esteso con aspetti legati al tempo, per spiegare la relazione tra tempo e trust. Infine quest’ultimo calcolo verrà applicato per dare una codifica del protocollo di routing per reti ad hoc chiamato ARAN.

Wireless systems consist of wireless devices which communicate with each other by means of a radio frequency channel. This networking paradigm offers much convenience, but because of the use of the wireless medium it is inherently vulnerable to many threats. As a consequence, security represents an important issue. Security mechanisms developed for wired systems present many limitations when used in a wireless context. The main problems stem from the fact that they operate in a centralised manner and under the assumption of a \closed world". Formal techniques are therefore needed to establish a mathematically rigorous connection between modelling and security goals. In the present dissertation we apply the well-known formalism of process calculus to model the features of wireless communication. The scientic contributions are primarily theoretical.We propose a timed process calculus modelling the communication features of wireless systems and enjoying some desirable time properties. The presence of time allows us to reason about communication collisions. We also provide behavioural equivalences and we prove a number of algebraic laws. We illustrate the usability of the calculus to model the Carrier Sense Multiple Access scheme, a widely used MAC level protocol in which a device senses the channel before transmitting. We then focus on security aspects, in particular we propose a trust model for mobile ad hoc networks, composed only of mobile nodes that communicate each other without relying on any base station. We model our networks as multilevel systems because trust relations associate security levels to nodes depending on their behaviour. Then we embody this trust model in a process calculus modelling the features of ad hoc networks. Our calculus is equipped with behavioural equivalences allowing us to develop an observational theory. We ensure safety despite compromised nodes and non interference results. We then use this calculus to analyse a secure version of a leader election algorithm for ad hoc networks. We also provide an encoding of the endairA routing protocol for ad hoc networks. Finally, we extend the trust-based calculus with timing aspects to reason about the relationship between trust and time. We then apply our calculus to formalise the routing protocol ARAN for ad hoc networks.