Il nuovo e sempre più popolare linguaggio di programmazione Rust è ampiamente utilizzato, dalle piccole startup alle più grandi aziende tecnologiche del mondo, per sviluppare sistemi operativi, browser web e altre applicazioni critiche per la sicurezza. Per la sua tesi di dottorato, in cui Jung ha gettato le prime basi formali per la programmazione di sistemi sicuri in Rust, ha già ricevuto diversi premi di fama internazionale.

Ralf Jung è ricercatore post-dottorato nel gruppo di ricerca "Fondamenti di programmazione" del professor Derek Dreyer presso il Max Planck Institute for Software Systems di Saarbrücken. Dal 2015, Jung si concentra sul linguaggio di programmazione originariamente sponsorizzato da Mozilla: "Rust mi ha entusiasmato perché ha un futuro molto promettente: essere un linguaggio di programmazione che consente un controllo preciso sull'utilizzo della memoria e sull'allocazione delle risorse in un sistema, evitando automaticamente molti errori di programmazione comuni", afferma Ralf Jung.

Il peso di questa promessa è dimostrato dall'uso pratico del linguaggio di programmazione: sebbene la prima versione stabile di Rust sia stata rilasciata solo nel 2015, il linguaggio è già utilizzato da molte grandi aziende tecnologiche come Microsoft, Google, Amazon, Dropbox e Facebook. Nella sua tesi di dottorato, Ralf Jung fornisce ora la prima prova formale che le promesse di sicurezza di Rust sono effettivamente mantenute.

"Siamo stati in grado di verificare la sicurezza del sistema di tipi di Rust e quindi di dimostrare come Rust eviti automaticamente e in modo affidabile intere classi di errori di programmazione", afferma Ralf Jung. In tal modo, ha anche affrontato con successo un aspetto particolare del linguaggio di programmazione: "La cosiddetta 'sicurezza dei tipi' va di pari passo con il fatto che Rust impone restrizioni al programmatore e non gli permette di fare tutto ciò che vorrebbe. Tuttavia, a volte è necessario scrivere un'operazione nel codice che Rust non accetterebbe a causa della sua sicurezza dei tipi", continua l'informatico. “È qui che entra in gioco una caratteristica speciale di Rust: i programmatori possono contrassegnare il proprio codice come ‘non sicuro’ se vogliono ottenere qualcosa che contraddice le precauzioni di sicurezza del linguaggio di programmazione. Insieme a collaboratori internazionali, tra cui il mio relatore di tesi Derek Dreyer, abbiamo sviluppato un quadro teorico che ci permette di dimostrare che le affermazioni di sicurezza di Rust rimangono valide nonostante la possibilità di scrivere codice ‘non sicuro’”, afferma Jung.

Questo test, chiamato RustBelt, è affiancato da uno strumento chiamato Miri, in grado di verificare automaticamente che il codice Rust ‘non sicuro’ sia conforme alle regole importanti della specifica Rust, un requisito fondamentale per la correttezza e la sicurezza di tale codice. “Mentre RustBelt ha riscosso un grande successo, soprattutto in ambito accademico, Miri è già affermato nel settore come strumento per testare la sicurezza dei programmi scritti in Rust”, spiega Ralf Jung.

Per la sua tesi di dottorato intitolata “Understanding and Evolution of the Rust Programming Language”, Ralf Jung ha ricevuto diversi premi nazionali e internazionali. Il lavoro di Jung ha ricevuto una delle due menzioni d'onore all'Association for Computing Machinery (ACM) Dissertation Award. L'ACM afferma: "Grazie alla leadership di Jung e al suo coinvolgimento attivo nel gruppo di lavoro Rust Unsafe Code Guidelines, il suo lavoro ha già avuto un profondo impatto sulla progettazione di Rust e ha gettato le basi essenziali per il suo futuro". L'ACM Dissertation Award viene assegnato a livello internazionale per l'intero campo dell'informatica ed è considerato uno dei premi più prestigiosi al mondo per le tesi di dottorato in informatica. Ha

inoltre ricevuto il Doctoral Dissertation Award dall'European Joint Conferences on Theory & Practice of Software (ETAPS), uno dei premi più importanti nel campo dell'informatica in Europa. Gli è stata anche conferita la medaglia Otto Hahn dalla Società Max Planck, assegnata annualmente per risultati scientifici particolarmente eccezionali relativi a una tesi di dottorato.

Ulteriori informazioni