Le langage de programmation Rust, récent et de plus en plus populaire, est largement utilisé, des jeunes entreprises aux géants de la tech, pour développer des systèmes d'exploitation, des navigateurs web et d'autres applications critiques pour la sécurité. Sa thèse de doctorat, dans laquelle Ralf Jung a posé les premiers fondements formels de la programmation de systèmes sécurisés en Rust, lui a déjà valu plusieurs prix internationaux prestigieux.

Ralf Jung est chercheur postdoctoral au sein du groupe de recherche « Fondements de la programmation » du professeur Derek Dreyer, à l'Institut Max Planck de recherche sur les systèmes logiciels de Sarrebruck. Depuis 2015, il se consacre à ce langage, initialement soutenu par Mozilla : « Rust m'a enthousiasmé car son avenir est prometteur : il offre un contrôle précis de l'utilisation de la mémoire et de l'allocation des ressources d'un système, tout en évitant automatiquement de nombreuses erreurs de programmation courantes », explique-t-il.

L'importance de cette promesse est démontrée par l'utilisation pratique du langage de programmation : bien que la première version stable de Rust n'ait été publiée qu'en 2015, le langage est déjà utilisé par de nombreuses grandes entreprises technologiques telles que Microsoft, Google, Amazon, Dropbox et Facebook. Dans sa thèse de doctorat, Ralf Jung apporte la première preuve formelle que les promesses de sécurité de Rust sont effectivement tenues.

« Nous avons pu vérifier la sécurité du système de types de Rust et ainsi montrer comment Rust évite automatiquement et de manière fiable des catégories entières d'erreurs de programmation », explique Ralf Jung. Ce faisant, il a également abordé avec succès un aspect particulier du langage : « La notion de "sécurité des types" est indissociable du fait que Rust impose des restrictions au programmeur et ne lui permet pas de faire tout ce qu'il souhaite. Cependant, il est parfois nécessaire d'écrire dans le code une opération que Rust refuserait en raison de sa sécurité des types », poursuit l'informaticien. « C’est là qu’intervient une particularité de Rust : les programmeurs peuvent marquer leur code comme “non sécurisé” s’ils souhaitent réaliser quelque chose qui contrevient aux mesures de sécurité du langage. Avec des collaborateurs internationaux, dont mon directeur de thèse, Derek Dreyer, nous avons développé un cadre théorique permettant de démontrer que les affirmations de sécurité de Rust restent valables malgré la possibilité d’écrire du code “non sécurisé” », explique Jung.

Ce test, appelé RustBelt, est complété par un outil nommé Miri, capable de vérifier automatiquement que le code Rust “non sécurisé” respecte les règles importantes de la spécification Rust – une condition essentielle à la correction et à la sécurité de ce code. « Si RustBelt a rencontré un vif succès, notamment dans le milieu universitaire, Miri est déjà bien implanté dans l’industrie comme outil de test de sécurité des programmes écrits en Rust », précise Ralf Jung.

Sa thèse, intitulée « Comprendre et l’évolution du langage de programmation Rust », a été récompensée par plusieurs prix nationaux et internationaux. Les travaux de Jung ont reçu l'une des deux mentions honorables du prix de thèse de l'Association for Computing Machinery (ACM). L'ACM déclare : « Grâce au leadership et à l'implication active de Jung au sein du groupe de travail Rust Unsafe Code Guidelines, ses travaux ont déjà eu un impact considérable sur la conception de Rust et ont jeté les bases essentielles de son avenir. » Le prix de thèse de l'ACM est décerné à l'échelle internationale pour l'ensemble du domaine de l'informatique et est considéré comme l'une des récompenses les plus prestigieuses au monde pour les thèses de doctorat en informatique. Il

a également reçu le prix de thèse de doctorat des Conférences conjointes européennes sur la théorie et la pratique du logiciel (ETAPS), l'une des plus importantes récompenses en sciences du logiciel en Europe. Il a également reçu la médaille Otto Hahn de la Société Max Planck, décernée chaque année pour des réalisations scientifiques exceptionnelles liées à une thèse.

Plus d'informations