Una tecnologia sviluppata dall’Università Ca’ Foscari Venezia per semplificare la creazione di strumenti di verifica del software è stata integrata come nuova funzionalità in una piattaforma globale di analisi dei programmi, Ghidra, progetto free e open source della National Security Agency (NSA) degli Stati Uniti. Il risultato porta un contributo della ricerca accademica italiana dentro un ecosistema open source molto diffuso tra chi si occupa di sicurezza informatica, analisi del codice e studio di software complessi. Strumenti come Ghidra, infatti, sono essenziali per la scoperta, il contenimento, e la neutralizzazione dei virus informatici.
La tecnologia nasce dal progetto di ricerca LiSA (Library for Static Analysis), sviluppato a Ca’ Foscari dal 2020 all’interno del gruppo di ricerca “Software and System Verification” (SSV) guidato dai professori Agostino Cortesi e Pietro Ferrara. L’obiettivo di LiSA è ridurre tempi e complessità necessari a costruire strumenti di “analisi e verifica formale” del software, cioè strumenti capaci di supportare, con metodi matematici rigorosi, il controllo di correttezza e sicurezza dei programmi.
L’integrazione è stata resa disponibile pochi giorni fa con il rilascio dell’ultima versione della piattaforma di analisi, un progetto open source sviluppato dalla National Security Agency e pubblicato per l’uso della comunità tecnologica internazionale.
Per la ricerca universitaria, si tratta di un riconoscimento importante: un’infrastruttura sviluppata in ambito accademico trova spazio in uno strumento largamente utilizzato e con impatto a livello internazionale.
«Quando una tecnologia sviluppata in università viene adottata in un progetto open source di ampia diffusione, il valore non è solo simbolico: significa che l’idea è utile, robusta e riusabile da una comunità ampia», dichiara Luca Negrini, ricercatore di Informatica dell’Università Ca’ Foscari Venezia e tra le persone che, assieme a Luca Olivieri e Vincenzo Arceri, hanno maggiormente contribuito allo sviluppo di LiSA. «Per noi è un passaggio importante: da un lato conferma l’impatto della nostra ricerca sui metodi formali e sull’analisi statica; dall’altro crea nuove opportunità per rendere più pratiche e accessibili tecniche che, tradizionalmente, richiedono lunghi tempi di sviluppo e competenze altamente specialistiche. In prospettiva, questo tipo di adozione può contribuire a migliorare qualità e sicurezza del software in contesti molto diversi.»
LiSA è oggi utilizzata dal team SSV di Ca’ Foscari sia in attività di ricerca, con una produzione scientifica consolidata, sia nella didattica, in particolare nei corsi dedicati all’analisi statica e alla verifica del software, contribuendo alla formazione di competenze avanzate in un settore cruciale per l’affidabilità dei sistemi digitali.
La tecnologia cafoscarina riguarda l’“analisi statica”, ovvero tecniche per individuare errori, vulnerabilità o proprietà del software che si applicano al codice sorgente e che si basano su solidi fondamenti logico-matematici, assicurando la correttezza dei risultati prodotti.
Questa attività di ricerca e sviluppo, co-finanziata dallo Spoke 6 “Sicurezza del software e delle piattaforme” del progetto PNRR SERICS, coordinato dall’Università Ca’ Foscari, è ulteriore riconoscimento della rilevanza dell’ateneo veneziano sui temi della Cybersecurity
