Il professor Francesco Ranzato, docente del Dipartimento di Matematica dell'Università di Padova, è stato premiato agli "Amazon Research Awards 2021" di Amazon Research - assieme a Roberto Giacobazzi dell’Università di Verona - per il progetto di ricerca dal titolo "Implicit Program Analysis": i due professori sono gli unici italiani assegnatari del riconoscimento di Amazon in questa edizione.

Amazon Research Awards

L’Amazon Research Awards, che comprende anche un finanziamento di 40.000 dollari e altri 20.000 in AWS credits da usare in servizi di calcolo di Amazon Web Services e coprirà una ricerca sviluppata su arco biennale, viene conferito alle migliori idee di ricerca in ambito “Ragionamento automatico”, in particolare per tecniche e strumenti di analisi statica dei programmi. L'analisi statica dei programmi è uno strumento automatico per identificare le loro vulnerabilità (i cosiddetti bug) che viene eseguito esaminando il codice senza eseguire direttamente il programma. L'analisi statica viene utilizzata dai team di sviluppo del software e di garanzia della sua qualità, in particolare dagli ingegneri del software di Amazon. Uno strumento automatico di analisi statica eseguirà la scansione di tutto il codice di un progetto software per verificare la presenza di errori logici e vulnerabilità, ad esempio di sicurezza, da segnalare agli ingegneri del software, che potranno quindi agire di conseguenza sul codice del programma per eliminarne gli errori. L’idea di ricerca premiata da Amazon si occupa quindi dell’adattamento del codice sorgente dei programmi affinché questo sia più precisamente analizzabile dagli strumenti di analisi statica. Questa tecnica innovativa di analisi statica dei programmi mira ad aiutare gli ingegneri del software nello sviluppo di un codice che sia conforme rispetto a standard elevati di correttezza e sicurezza, ad esempio quelli dei team di sviluppo del software di Amazon. «Esempi classici di bug individuati dagli strumenti di analisi statica dei programmi - spiega Francesco Ranzato - sono le falle di sicurezza ed i valori mal definiti, che possono causare problemi potenzialmente disastrosi, come attacchi da parte di hacker o malfunzionamenti di software critico usato in ambito aerospaziale o medico. Lo scopo di questa ricerca premiata da Amazon è aumentare la precisione degli strumenti di analisi statica adattando a priori il codice sorgente alle capacità dello strumento di analisi statica di individuare gli errori. La conformità del codice sorgente alle potenzialità degli strumenti di analisi statica è una frontiera di ricerca largamente inesplorata, e con questo progetto miriamo a progettare dei metodi per sintetizzare automaticamente dei programmi che siano conformi alle principali analisi statiche, in particolare per garantire la sicurezza dei programmi».