Ogni volta che acquisti qualcosa su Amazon, i dati dei tuoi clienti vengono automaticamente aggiornati e archiviati su migliaia di macchine virtuali nel cloud. Per aziende come Amazon, è essenziale garantire la sicurezza e la protezione dei dati dei suoi milioni di clienti. Questo vale sia per le organizzazioni grandi che per quelle piccole. Ma fino ad ora, non c'era modo di garantire che un sistema software fosse protetto da bug, hacker e vulnerabilità.
I ricercatori della Columbia Engineering potrebbero aver risolto questo problema di sicurezza. Hanno sviluppato SeKVM, il primo sistema che garantisce, attraverso prove matematiche, la sicurezza delle macchine virtuali nel cloud. In un nuovo documento che sarà presentato il 26 maggio 2021, al 42° IEEE Symposium on Security & Privacy, i ricercatori sperano di gettare le basi per future innovazioni nella verifica del software di sistema, portando a una nuova generazione di software di sistema cyber-resiliente.
SeKVM è il primo sistema formalmente verificato per il cloud computing. La verifica formale è un passaggio fondamentale in quanto è il processo per dimostrare che il software è matematicamente corretto, che il codice del programma funziona come dovrebbe e non ci sono bug di sicurezza nascosti di cui preoccuparsi.
"Questa è la prima volta che un sistema software multiprocessore del mondo reale ha dimostrato di essere matematicamente corretto e sicuro", ha affermato Jason Nieh, professore di informatica e co-direttore del Software Systems Laboratory. "Ciò significa che i dati degli utenti sono gestiti correttamente dal software in esecuzione nel cloud e sono al sicuro da bug di sicurezza e hacker".
La costruzione di un software di sistema corretto e sicuro è stata una delle grandi sfide del computing. | Nieh ha lavorato su diversi aspetti dei sistemi software da quando è entrato a far parte della Columbia Engineering nel 1999. Quando Ronghui Gu, l'assistente professore di informatica della famiglia Tang ed esperto di verifica formale, è entrato a far parte del dipartimento di informatica nel 2018, lui e Nieh hanno deciso di collaborare sull'esplorazione della verifica formale dei sistemi software.
La loro ricerca ha suscitato grande interesse: entrambi i ricercatori hanno vinto un Amazon Research Award, molteplici sovvenzioni dalla National Science Foundation e un contratto multimilionario della Defense Advanced Research Projects Agency (DARPA) per promuovere lo sviluppo del progetto SeKVM. Inoltre, Nieh ha ricevuto una borsa di studio Guggenheim per questo lavoro.
Negli ultimi dodici anni è stata prestata molta attenzione alla verifica formale, compreso il lavoro sulla verifica dei sistemi operativi multiprocessore. "Ma tutta questa ricerca è stata condotta su piccoli sistemi simili a giocattoli che nessuno usa nella vita reale", ha detto Gu. "Si è ritenuto che la verifica di un sistema commodity multiprocessore, un sistema ampiamente utilizzato come Linux, fosse più o meno impossibile".
La crescita esponenziale del cloud computing ha consentito alle aziende e agli utenti di spostare i propri dati e calcoli fuori sede in macchine virtuali in esecuzione su host nel cloud. I provider di cloud computing, come Amazon, implementano hypervisor per supportare queste macchine virtuali
Un hypervisor è il software chiave che rende possibile il cloud computing. La sicurezza dei dati della macchina virtuale dipende dalla correttezza e dall'affidabilità dell'hypervisor. Nonostante la loro importanza, gli hypervisor sono complicati: possono includere un intero sistema operativo Linux. Solo un singolo anello debole nel codice, virtualmente impossibile da rilevare tramite i test tradizionali, può rendere un sistema vulnerabile agli hacker. Anche se un hypervisor è scritto correttamente al 99%, un hacker può comunque intrufolarsi in quella particolare configurazione dell'1% e prendere il controllo del sistema.
Il lavoro di Nieh e Gu è il primo a verificare un sistema di merci, in particolare l'hypervisor KVM ampiamente utilizzato, che viene utilizzato per eseguire macchine virtuali da provider di cloud come Amazon. Hanno dimostrato che SeKVM, che è KVM con alcune piccole modifiche, è sicuro e garantisce che i computer virtuali siano isolati l'uno dall'altro.
"Abbiamo dimostrato che il nostro sistema è in grado di proteggere e proteggere i dati privati e l'informatica caricati nel cloud con garanzie matematiche", ha affermato Xupeng Li, Ph.D. di Gu. studente e co-autore dell'articolo. "Questo non è mai stato fatto prima."
SeKVM è stato verificato utilizzando MicroV, un nuovo framework per la verifica delle proprietà di sicurezza di sistemi di grandi dimensioni. Si basa sull'ipotesi che piccole modifiche al sistema possano rendere significativamente più facile la verifica, una nuova tecnica che i ricercatori chiamano verifica MICR. Questa nuova tecnica di stratificazione aggiorna un sistema esistente ed estrae i componenti che rafforzano la sicurezza in un piccolo nucleo che viene verificato e garantisce la sicurezza dell'intero sistema.
Le modifiche necessarie per il retrofit di un sistema di grandi dimensioni sono piuttosto modeste: i ricercatori hanno dimostrato che se il piccolo nucleo del sistema più grande è intatto, il sistema è sicuro e non verranno divulgati dati privati. È così che sono stati in grado di verificare un sistema di grandi dimensioni come KVM, che in precedenza si pensava fosse impossibile.
"Pensa a una casa: una crepa nel muro a secco non significa che l'integrità della casa sia a rischio", ha spiegato Nieh. "È ancora strutturalmente solido e il sistema strutturale chiave è buono."
Shih-Wei Li, dottorato di ricerca di Nieh. studente e co-autore principale dello studio, ha aggiunto: "SeKVM servirà da salvaguardia in vari domini, dai sistemi bancari e dai dispositivi Internet of Things ai veicoli autonomi e alle criptovalute".
In qualità di primo hypervisor commodity verificato, SeKVM potrebbe cambiare il modo in cui i servizi cloud dovrebbero essere progettati, sviluppati, implementati e affidabili. In un mondo dove sicurezza informatica è una preoccupazione crescente, questa resilienza è molto richiesta. Le principali aziende cloud stanno già esplorando come possono sfruttare SeKVM per soddisfare questa domanda.