Processori a prova di hacker. A Matteo Busi il premio di Cybersecurity

“I processori sono un po’ ovunque: nei pc, in tutte le cose smart, come lo smartphone, il frigo, la lavatrice, l’automobile. Ma sono anche - per esempio - nei pacemaker, strumenti vitali che processano il segnale cardiaco di un paziente. E i processori possono essere hackerati, il rischio è nella vita di tutti i giorni ed è concreto. Noi, grazie a un modello matematico, abbiamo realizzato uno scudo informatico impenetrabile.”

Così Matteo Busi, ricercatore presso il Dipartimento di Scienze Ambientali, Informatica e Statistica di Ca’ Foscari, racconta la sua ricerca in materia di Cybersecurity, che l’ha portato a essere tra i 10 vincitori del Premio Giovani Ricercatori, assegnato dal Gruppo 2003 e dedicato alle ricercatrici e ai ricercatori con meno di 7 anni di attività dalla fine del dottorato. 

Lo scorso 6 novembre presso la sede centrale del Consiglio nazionale delle ricerche a Roma, alla presenza della presidente del CNR Maria Chiara Carrozza, Matteo si è aggiudicato il premio di Cybersecurity con un lavoro che presenta una metodologia per estendere in modo sicuro le funzionalità di un microprocessore e garantire la sicurezza degli utenti e delle applicazioni.

Lo studio Securing Interruptible Enclaved Execution on Small Microprocessors del 2021 è iniziato durante il periodo di dottorato di Matteo ed è co-realizzato con altri 6 autori, tra cui il prof. Frank Piessens della DistriNet Research Unit di KU Leuven.

E’ il risultato di un lavoro di squadra a livello internazionale, e si concentra  su un problema ampio e diffuso: l’impatto potenziale degli attaccanti - i cosiddetti ‘hacker’ - sui dispositivi che usiamo tutti i giorni, come laptop, desktop, server, smartphone, smartwatch. Ci siamo focalizzati sul processore MSP430 della Texas instruments, uno dei più economici, utilizzato in moltissimi strumenti di uso quotidiano in mano a ciascuno di noi. 

Un gruppo di ricerca dell’Università di Ku Leuven aveva già esteso la sicurezza di questo processore, chiamato poi Sancus, ma ne evidenziava ancora alcune vulnerabilità. Abbiamo quindi sviluppato un modello matematico che teneva conto del comportamento del processore, dei possibili attacchi e della loro interazione. Il modello ci ha permesso di mappare tutte le possibili falle del sistema, anche quelle che non erano ancora state prese in considerazione. Abbiamo quindi esteso la sicurezza del processore senza diminuire le proprietà di performance del dispositivo, e abbiamo dimostrato attraverso una prova matematica che il nostro intervento ha reso il processore inattaccabile quasi al 100%.

Premetto che sono un ricercatore e i miei studi hanno tante applicazioni nella cybersecurity, ma non sono un hacker in grado di entrare in un pc come nei film. Nel mondo accademico ci si occupa  della difesa per capire come agiscono o potrebbero agire gli attaccanti, si cerca la vulnerabilità della struttura interna dei processori, e si ipotizza come si potrebbero estrarre informazioni che non dovrebbero essere estratte. 

Spectre e Meltdown sono due attacchi considerati fra i più pericolosi. Gli hacker hanno approfittato di vulnerabilità intrinseche dei processori per estrarre informazioni segrete, senza lasciare nessuna traccia, come il numero della carta di credito dall’applicazione della banca oppure le chiavi crittografiche per cifrare le info delle app di messaggistica. Questo è quello che conosciamo, ma possiamo immaginare ci sia tanto altro che avviene e di cui non sappiamo nulla. In alcuni casi sono gli stessi Stati a finanziare alcuni gruppi di hacker.

I colleghi di Ku Leuven si sono accorti che il prototipo di processore esteso Sancus era vulnerabile ad un attacco capace di usare strutture interne del processore stesso per estrarre informazioni segrete e manipolare il comportamento del programma, facendo deragliare il suo comportamento anche verso azioni malevole.

Abbiamo formulato un modello matematico del prototipo del processore. Su questo modello abbiamo aggiunto un modello matematico già esistente degli attaccanti, ossia tutto l’insieme di azioni che l’attaccante può fare, come osservare quello che viene fatto, creare un codice che viene eseguito sul processore, manipolare quello che può essere caricato in memoria, dare input e far eseguire i suoi programmi. Il nostro studio è servito a dimostrare che su quel modello si poteva ridisegnare il processore, rendendolo inattaccabile.

Sappiamo quali azioni può fare un hacker, ma non sappiamo come può combinarle: grazie al modello, in qualunque modo le combini, il processore non può essere violato.

Il modello matematico, che tecnicamente si chiama semantica del processore, spiega come, dato un programma, il processore si comporterà, e descrive infiniti comportamenti, rendendo il processore inattaccabile contro gli attaccanti considerati.

Uno scudo informatico impenetrabile?

Direi di sì, la nostra dimostrazione, lunga e complessa, è frutto di sette co-autori, numerose prove e peer review. 

Lavoro su questi temi con il gruppo di Cybersecurity guidato da Riccardo Focardi e Flaminia Luccio. Insieme a loro, dopo che i colleghi di Leuven hanno trovato discrepanze tra il modello matematico e la realtà, abbiamo sviluppato una metodologia per derivare dei modelli semplificati e cercare gli attacchi in automatico. Il nuovo sistema effettua prove contro un attaccante che assomiglia a quello del lavoro premiato, in modo da garantire che le dimostrazioni non abbiano errori.

Spesso i livelli di performance e la sicurezza sono inversamente proporzionali. La produzione della maggior parte dei prodotti tecnologici sviluppati in questi ultimi anni non ha tenuto sufficientemente conto della sicurezza, puntando sulla performance, sulla velocità dei dispositivi. L’investimento nella sicurezza informatica è però in costante crescita per le aziende che utilizzano processori, come per esempio l’intero comparto dell’automotive.