Ricerca di contatti, progetti,
corsi e pubblicazioni

Detection of Security Flaws and Vulnerabilities by Guided Model Checking

Persone

Responsabili

Sharygina N.

(Responsabile)

Abstract

L´informazione è un´importante risorsa strategica ed operazionale e nasce perciò la necessità di disporre di adeguate misure di sicurezza che possano salvaguardare l´informazione sensibile. La sicurezza dei sistemi di computer comporta diversi aspetti, che spaziano dalla crittografia alle implementazioni di sicurezza di basso livello. La maggior parte degli esempi pratici è basata sui difetti d´implementazione piuttosto che sui difetti dei principi o dei protocolli crittografici. Nonostante la sua importanza, non vi sono studi di ricerca esaurienti riguardanti la sicurezza delle implementazioni di basso livello. Questo progetto si prefigge di comprendere i problemi di sicurezza dell´informazione, di integrità e di disponibilità nel software garantendo la sicurezza dell´implementazione effettiva in un linguaggio come ANSI-C.
Tra gli argomenti specifici di interesse vi sono: 1) la valutazione della vulnerabilità; 2) l´individuazione dei difetti del software; e di conseguenza 3) la protezione dal codice che potrebbe arrecare danni.
Le tecniche esistenti per garantire le proprietà di sicurezza sono per la maggior parte tecniche ad hoc ed informali. Al contrario, questo progetto si propone di sviluppare delle tecniche esaustive che garantiscano formalmente la correttezza delle proprietà di sicurezza. La tecnologia "Model Checking" è perfettamente adatta a questo scopo.
"Model checking" esamina in modo esaustivo tutti gli stati possibili che il software potrebbe assumere in modo da individuare le possibili violazioni della proprietà in questione. Tuttavia "Model checking" pone il problema dell´esplosione del numero dei possibili stati: la sua dimensione, ad esempio, supera spesso la capacità dello strumento di Model Checking. Quando si applica Model Checking a software su larga scala, la principale sfida della ricerca è proprio il problema della scalabilità. Noi proponiamo di adattare gli algoritmi che riducono il numero degli stati in modo da poterli utilizzare per il software che garantisce la sicurezza, e di sviluppare in questo modo un modello specialistico che verifichi gli algoritmi per individuare la vulnerabilità dal punto di vista della sicurezza.
L´idea principale è quella di ricavare dei modelli guida per indirizzare la ricerca effetuata dai cosiddetti "symbolic model checker" verso quelle aree che verosimilmente contengono vulnerabilità e di utilizzare questi modelli guida per generare più rapidamente le prove dell´assenza di queste vulnerabilità. Le tecniche guida che proponiamo di esplorare sono relative al comportamento del componente software, all´apprendimento di un linguaggio per descrivere il comportamento normale, e mettere a disposizione alcuni modelli campione.

Informazioni aggiuntive

Data d'inizio
01.10.2006
Data di fine
01.10.2008
Durata
24 Mesi
Enti finanziatori
Stato
Concluso
Aree di ricerca
P170 Computer science, numerical analysis, systems control
P175 Informatics, systems theory