Proposte di tesi
Le tesi proposte si inquadrano in attività di ricerca riguardanti
le tecniche per lo sviluppo del software basate su approcci formali.
Queste tecniche impiegano strumenti sofisticati, che automatizzano buona
parte della produzione del software e consentono di ottenere elevati
standard qualitativi, soprattutto in termini di correttezza.
Si applicano pertanto al software classificato come critico che, come noto,
è sempre più pervasivo e va dalle applicazioni safety critical
(avioniche, automotive, industriali, medicali) alle applicazioni security
critical (quelle che devono garantire il corretto funzionamento anche in
ambienti ostili).
Le attività di ricerca in cui le tesi proposte si inseriscono sono
focalizzate soprattutto sul software distribuito e concorrente e mirano a
sperimentare e migliorare gli strumenti e le metodologie di sviluppo.
- Sviluppo Model-based di applicazioni security-aware in Java
- Qualificazione di strumenti software per applicazioni critiche
- Generazione automatica di test funzionali a partire da modelli semi-formali
Per ulteriori informazioni: Prof. Riccardo Sisto (Tel. 011 090 7073)
Sviluppo Model-based di applicazioni security-aware in Java
Un'applicazione è security-aware se comprende esplicitamente la logica
per la gestione degli aspetti di security, usando tecniche quali
password, crittografia e protocolli crittografici.
La gestione della security è un aspetto critico nella programmazione
e svilupparla in modo corretto, cioè senza introdurre falle di
sicurezza, è tutt'altro che banale.
Per questo motivo, esistono tecniche di supporto allo sviluppo, che
hanno l'obiettivo di innalzare la confidenza nella corretta
implementazione. Tra di esse vi è l'approccio model-based, che consiste
nel costruire prima un modello astratto dell'applicazione, focalizzato
sulle parti rilevanti per la security. Questo modello è sufficientemente
semplice da poter essere analizzato automaticamente per verificare che
effettivamente raggiunga gli obiettivi di security desiderati.
Dal modello astratto si sviluppa poi l'implementazione in linguaggio
di programmazione, avvalendosi di strumenti di generazione automatica
del codice.
Uno dei problemi dell'approccio model-based è che i linguaggi di
modellazione quali l'UML o altri linguaggi domain-specific sono spesso
considerati ostici e non congegnali al programmatore, oltre ad essere
non universalmente noti.
L'obiettivo di questa tesi è sperimentare un diverso approccio alla
modellazione delle applicazioni security-aware, nel quale il modello
astratto viene formulato usando lo stesso linguaggio di programmazione a
oggetti Java e il relativo meccanismo delle annotazioni. Questo
semplifica la modellazione per i programmatori che già conoscono questo
linguaggio.
Il lavoro della tesi consiste nello studiare questo nuovo approccio
alla modellazione, già proposto in una tesi precedente, e nell'usarlo
per sviluppare implementazioni di protocolli di autenticazione standard
quali SSH o SSL. Lo sviluppo arriverà fino alla realizzazione di
un'applicazione completa, della quale verrà testata l'interoperabilità
con altre implementazioni di terze parti.
Una possibilità alternativa è
lavorare al framework di sviluppo model based per estenderne le
caratteristiche.
In entrambi i casi, la tesi consente di approfondire la
programmazione Java e la metodologia di sviluppo model-based, che si sta
rapidamente diffondendo in diversi ambiti dello sviluppo di software.
Qualificazione di strumenti software per applicazioni critiche
Gli strumenti software che vengono usati nello sviluppo di sistemi
critici per la sicurezza (per esempio sistemi avionici o, sempre più
spesso, anche sistemi automotive) devono essere "qualificati", cioè aver
subito una valutazione che li attesta come "attendibili" per essere
impiegati in quel contesto. Tali valutazioni in genere partono da
un'analisi del rischio, che deve valutare gli effetti dei potenziali
errori che il software potrebbe commettere a causa di bachi. Questa
analisi, per esempio, potrebbe evidenziare che certi moduli del software
non sono in realtà critici perchè eventuali errori in essi non hanno
conseguenze gravi. Altri moduli invece sono critici e devono quindi
essere testati in modo più accurato.
Scopo della tesi è sperimentare la tecnica FMEA (Filure Modes and
Effects Analysis) per fare un'analisi di rischio su un software
commerciale, in collaborazione con l'azienda che produce quel software.
La tesi consente di imparare la tecnica FMEA e di entrare in contatto con una realtà industriale di sviluppo software.
Generazione automatica di test funzionali a partire da modelli semi-formali
Lo sviluppo model-based del software parte da modelli di alto livello,
che possono essere espressi tramite linguaggi grafici semi-formali come
UML e suoi derivati.
Una tecnica che si sta affermando recentemente è il model-based
testing, cioè la generazione automatica di test funzionali a partire dai
modelli che descrivono i requisiti del software.
La tesi si propone di realizzare un ambiente di model-based testing
che sia in grado di generare i test a partire da requisiti espressi con
linguaggi derivati da UML, come il SysML.
Ultima modifica: Ottobre 2011