Un podio mondiale per la cyber security italiana: LiSA, il framework open source per la verifica del software sviluppato dall’Università Ca’ Foscari di Venezia, ha conquistato il terzo posto a SVCOMP 2026, la principale competizione internazionale del settore organizzata in occasione della conferenza accademica Tools and Algorithms for the Construction and Analysis of Systems (TACAS), una delle maggiori conferenze mondiali in ambito di verifica software..
Unica tecnologia 100% made in Italy in gara, JLiSA – l’estensione per l’analisi di codice Java – si è classificata dietro ai progetti JBMC e GDart, confermando la rilevanza della ricerca italiana su uno dei temi cruciali della sicurezza informatica: la qualità e la sicurezza del codice.
L’attività di ricerca e sviluppo italiana è co-finanziata dallo Spoke 6 “Sicurezza del software e delle piattaforme” del progetto PNRR SERICS coordinato proprio dalla Ca’ Foscari con il Prof. Riccardo Focardi, a conferma della rilevanza italiana su uno dei temi cruciali della cyber security: la sicurezza del codice.
Inoltre, LiSA è stata integrata dalla NSA all’interno di Ghidra, uno strumento open source per l’analisi di programmi compilati. Lo strumento si candida a pieno titolo come possibile incentivo all’adozione di tecnologia italiana per l’analisi statica del codice.
Indice degli argomenti
Progetto LiSA per l’analisi del software: evoluzione del progetto
LiSA offre un framework generico che può essere applicato a diversi linguaggi di programmazione e tecnologie.
La tecnologia nasce inizialmente come prodotto della tesi di dottorato industriale in Informatica di Luca Negrini, concluso nel 2023 a Ca’ Foscari. Il progetto è stato portato avanti all’interno del gruppo di ricerca “Software and System Verification” (SSV) guidato dai professori Agostino Cortesi e Pietro Ferrara.
Negli ultimi mesi, LiSA è stato esteso per l’analisi di programmi Java (JLisa). Grazie a un lavoro di squadra che ha coinvolto ricercatori e dottorandi cafoscarini (lo stesso Luca Negrini, Luca Olivieri, Giacomo Zanatta e Teodors Lisovenko) in collaborazione con l’Università di Parma, e in particolare con il ricercatore Vincenzo Arceri e lo studente magistrale Filippo Bianchi.
Luca Negrini ne spiega gli elementi fondanti: “LiSA (Library for Static Analysis) è una libreria open source per l’analisi statica del software.
A differenza dell’analisi dinamica, che esegue il programma su casi di test specifici, l’analisi statica in generale e LiSA in particolare, esaminano il codice sorgente senza eseguirlo, identificando potenziali errori e vulnerabilità.
La libreria è basata sulla teoria dell’Interpretazione astratta, un framework matematicamente fondato, che permette di ragionare su tutte le possibili esecuzioni di un programma in modo ‘sound’, ovvero corretto, e fornisce quindi garanzie formali sui suoi risultati”.
La soundness ovvero la correttezza del codice o di un sistema logico indica che le regole inferenziali o i processi di analisi applicati producono solo risultati veri o validi. Se un sistema è ‘sound’, ciò che afferma di aver provato o verificato è effettivamente corretto, garantendo assenza di falsi positivi nelle analisi.
Caratteristiche ed estensioni del progetto
La modularità è un’altra caratteristica distintiva: “LiSA è modulare e supporta più linguaggi tramite front-end specializzati: oltre a JLiSA per Java, esistono front-end per Python, Go, smart contract Ethereum e Tezos. Qualche mese fa, inoltre, LiSA è stata integrata dalla NSA all’interno di Ghidra, uno strumento open source per l’analisi di programmi compilati”.
Ma c’è di più. “La flessibilità ed estendibilità di LiSA permettono di applicare tale libreria a una molteplicità di analisi e proprietà, anche in ambito di sicurezza”.
Esempi di questa varianza sono stati anche oggetto di pubblicazioni scientifiche. “GoLiSA (pubblicata con paper nell’ambito del 37th European Conference on Object-Oriented Programming – ECOOP 2023) esegue una serie di controlli di vario tipo su codice blockchain (ad esempio, Hyperledger Fabric) scritto in Go. Un’altra estensione di LiSA su codice Python per ROS2 (cui è dedicata una ulteriore pubblicazione) si è focalizzata sull’estrazione e verifica di policy di sicurezza.
Evidenze dell’analisi per irrobustire il codice
La libreria facilita l’introduzione di remediation di chiusura bug o di correzione errori perché “produce segnalazioni precise che indicano esattamente dove nel codice si trovino i potenziali problemi: file, riga, e tipologia di errore. Gli sviluppatori sanno quindi esattamente dove intervenire e di che natura è il problema (ad es. la possibile ‘NullPointerException’, violazione di un contratto, comportamento non deterministico). Questo rende la correzione degli errori molto più rapida e mirata rispetto a strumenti che restituiscono segnalazioni generiche”.
Una proprietà peculiare è la soundness ovvero la correttezza. Luca Negrini sottolinea in questo senso che “la caratteristica più importante è la soundness garantita dall’Interpretazione Astratta: quando LiSA non segnala un errore di una certa categoria, questa assenza è matematicamente provata ovvero non è una stima statistica”, il tutto in favore della eliminazione dei falsi positivi.
“Questo elimina i falsi negativi, ovvero i bug che sfuggono all’analisi e che negli strumenti tradizionali (come il testing o analisi euristiche) possono dare una falsa sicurezza agli sviluppatori. In pratica: se LiSA dice che il codice è privo di ‘null pointer exception’, lo è davvero in ogni possibile scenario di esecuzione”.
Future evoluzioni del progetto per l’adozione di tecnologia italiana
Entrambe i docenti chiariscono che “LiSA è stato un progetto universitario e di ricerca, per cui la sua integrazione con ambienti di sviluppo e la sua commercializzazione non sono state ancora affrontate, anche se rientrano nella roadmap”.
Naturalmente esistono possibili sviluppi futuri. “Abbiamo in mente svariati sviluppi futuri: estensione a nuovi linguaggi e piattaforme (Python con FastAPI, Java con Spring, C++), miglioramento della precisione delle analisi per ridurre ulteriormente i falsi positivi, ed ovviamente la partecipazione alle future edizioni di SV-COMP con risultati, si spera, sempre più competitivi”.
L’orientamento alla creazione di una Start up esiste ma non è ancora avviato mentre il team è aperto a collaborazioni.
“Attualmente non esiste una startup commerciale dedicata, anche se stiamo valutando proprio ora questa opzione, considerato anche una parte considerevole del team viene da un’esperienza di commercializzazione di un tool simile (ulia, spin-off nata nel 2010 a Verona dall’iniziativa del prof. Spoto, n.d.r.), ma il codice è interamente open source e il gruppo SSV è aperto a collaborazioni sia con aziende che con altri gruppi di ricerca”.
Lo strumento è attualmente adottato in diversi contesti anche internazionali esterni all’accademia. “LiSA è già adottata in contesti didattici universitari e di ricerca applicata in diversi domini (blockchain, robotica, microservizi, data science), e l’integrazione in Ghidra – uno strumento con una comunità globale molto ampia – dimostra l’interesse per questo strumento ben oltre l’ambito accademico”.
Non resta che verificare l’interesse delle realtà italiane che ora potrebbero avere una scelta integralmente italiana per il controllo statico del codice sorgente.
La competizione SV_COMP 2026
La quindicesima edizione della competizione mondiale nel settore della verifica del software (Competition on Software Verification, SV-COMP) svolta a Torino per la categoria “Java Verification” ha premiato come terzo classificato il progetto Italiano JLISA (Library for Static Analysis), unica tecnologia 100% made in Italy. I progetti open source JBMC e a GDart rispettivamente sono risultati primo e secondo classificato.
La competizione nasce per stimolare l’invenzione di nuovi metodi, tecnologie e strumenti e offrire una panoramica sullo stato dell’arte della verifica del software, dando visibilità e riconoscimento agli sviluppatori.
Nonostante le difficoltà per il test dei diversi prototipi presentati, la SV-COMP utilizza un set consolidato di attività di verifica per confrontare i verificatori di software (disponibili sul proprio sito) che fungono anche da benchmark per la verifica del software nella comunità. Pietro Ferrara, professore responsabile del team di ricerca che ha sviluppato il framework LiSA e Luca Negrini Professore assistente e PhD dalla cui tesi di dottorato nasce Lisa, spiegano che: “SV-COMP utilizza benchmark, che coprono diverse categorie di proprietà verificabili: assenza di errori a runtime (accessi a puntatori nulli, buffer overflow), corretta gestione della memoria, rispetto di requisiti funzionali tramite assert, etc. Si tratta per lo più, di controlli sulla qualità in generale del codice”.
