Nicola e la sua passione per il computer

Nicola Cuomo, 27 anni, di Aversa, si è laureato lo scorso marzo in Informatica. Per realizzare la sua tesi di laurea, ha lavorato, insieme al prof. Adriano Peron, alla modellizzazione di protocolli di sicurezza, indipendenti dal tempo. Un protocollo è l’insieme delle regole che descrivono, in maniera formale, il modo in cui gli utenti coinvolti partecipano alla comunicazione. Per chi usa internet, la sigla http rappresenta un protocollo di comunicazione. Nella maggior parte di essi, ci si astrae dal tempo. “Noi, invece, abbiamo esteso il linguaggio, per tenere conto anche dei vincoli temporali e definire, in maniera precisa, l’evoluzione del protocollo” spiega Nicola. La sua passione per l’informatica è antica “ho sempre immaginato la mia vita insieme ai computer. Da piccolo me ne hanno regalato uno e mi sono subito appassionato. Era una cosa magica, funzionava e non sapevi perché. Capire le varie applicazioni mi ha sempre affascinato”. Proprio la curiosità ha nutrito, fin dalla scuola, la sua passione per la scienza. “Si parte da cose in realtà molto semplici, quasi banali, che messe insieme danno origine a risultati complessi”. Quando si è iscritto all’università, non aveva ancora compiuto 18 anni e l’unico corso di laurea in Informatica era, allora, a Salerno. Scelse, quindi, Ingegneria Informatica. “Quando è nato il Corso di Laurea in Informatica qui a Scienze mi sono trasferito”. Il futuro è ancora incerto. Nicola ha, al momento, un contratto di dieci mesi con l’università per proseguire il suo lavoro.  Gli è stato anche proposto il dottorato ed il concorso si svolge a settembre. La scelta è tra la ricerca e il lavoro. “Lavorare all’università, permette di gestirsi il proprio tempo. In un’azienda sarei più vincolato, ma guadagnerei meglio. Mi sento più portato per le cose pratiche, credo che il lavoro metterebbe in evidenza questo aspetto, ma ho ancora tempo per decidere”. La verifica di modelli, il model-checking è uno dei campi più sviluppati dell’informatica. Quasi tutto quello che si fa, prevede di dover verificare un modello. Il linguaggio sul quale il gruppo napoletano ha lavorato è il frutto di un progetto di ricerca europeo, cui hanno contribuito l’università di Genova e industrie tecnologiche come la Siemens. “Specificare un protocollo in maniera formale è, di per se, poco importante. Il nostro obiettivo era verificare che, dati determinati requisiti, il protocollo li soddisfacesse tutti. La nostra concentrazione era maggiormente rivolta ai protocolli di sicurezza” prosegue il giovane laureato. I protocolli più conosciuti sono in chiaro. Non solo gli utenti direttamente coinvolti, mittente e destinatario, possono avere accesso alle informazioni ma anche un’eventuale terza parte, che monitora il canale, può accedere alla comunicazione. In protocollo di sicurezza questo non può avvenire. “Dovevamo verificare che i protocolli soddisfacessero i requisiti di segretezza e autenticazione. Per farlo era necessario definire questo protocollo in termini di automi temporizzati”. Gli automi non sono macchine, ma formalismi che descrivono sistemi a transizione. Antecedenti alla nascita delle macchine fisiche, modellano la computazione e spiegano come questa avvenga. Gli automi temporizzati permettono di definire anche il tempo dell’applicazione. Il passaggio dal linguaggio di specifica, quello con cui viene creato il protocollo, al nuovo formalismo, è importante perché permette di applicare tutta una serie di teorie relative alla verifica automatica di modelli. Il lavoro di Nicola ha riguardato l’estensione del linguaggio e l’individuazione delle caratteristiche temporali più interessanti da specificare. È stato anche sviluppato un programma che esegue la traduzione in maniera automatica. “Si da in pasto alla macchina un file di testo, contenente la specifica del protocollo. Il risultato è un file con l’automa che lo descrive. Il tutto finisce in un verificatore di modelli, per controllare che le proprietà richieste siano soddisfatte. Siamo riusciti ad ottenere un prototipo e verificato un protocollo”. Bisogna, però, ancora migliorare la resa del programma. Il prototipo, infatti, impiega troppo tempo per la verifica di protocolli complessi e gli studi proseguiranno naturalmente in questa direzione. Le possibilità di utilizzo di questi sistemi sono molte, soprattutto pensando alle applicazioni in rete, ma si tratta comunque di piccoli frammenti. Le implementazioni reali devono tenere conto di strutture più ampie. I risultati di questo lavoro si ritroveranno in altre procedure reali, ad esempio nei processi di autenticazione. “Anche se con molte scale di grigi, verifichiamo la veridicità di un modello teorico, astraendo quello che può essere applicato o meno” conclude Nicola.
Simona Pasquale
- Advertisement -





Articoli Correlati