Ralf Jung, estudiante de doctorado de la Universidad de Saarland y ahora postdoc en el Instituto Max Planck de Sistemas de Software de Saarbrücken, ha realizado una importante contribución a la seguridad del lenguaje de programación "Rust".

El nuevo y cada vez más popular lenguaje de programación se utiliza ampliamente desde pequeñas empresas emergentes hasta las mayores corporaciones tecnológicas del mundo para desarrollar sistemas operativos, navegadores web y otras aplicaciones de seguridad crítica. Por su tesis doctoral, en la que Jung estableció los primeros fundamentos formales para la programación de sistemas seguros en Rust, ha recibido ya varios premios de renombre internacional.

Ralf Jung es investigador postdoctoral en el grupo de investigación "Fundamentos de la programación" del profesor Derek Dreyer en el Instituto Max Planck de Sistemas de Software de Saarbrücken. Desde 2015, Jung se ha centrado en el lenguaje de programación que originalmente fue patrocinado por Mozilla: "Rust me entusiasmó porque hay una futuro muy tentador detrás: ser un lenguaje de programación que permite un control preciso sobre el uso de la memoria y la asignación de recursos de un sistema, al tiempo que evita automáticamente muchos errores de programación generalizados", dice Ralf Jung.

El peso de esta promesa lo demuestra el uso del lenguaje de programación en la práctica: Aunque la primera versión estable de Rust no se publicó hasta 2015, el lenguaje de programación ya es utilizado por muchas grandes empresas tecnológicas como Microsoft, Google, Amazon, Dropbox y Facebook. En su tesis doctoral, Ralf Jung aporta ahora la primera prueba formal de que las promesas de seguridad de Rust se cumplen realmente.

"Hemos sido capaces de verificar la seguridad del sistema de tipos de Rust y, por tanto, mostrar cómo Rust evita de forma automática y fiable clases enteras de errores de programación", afirma Ralf Jung. Al hacerlo, también abordó con éxito un aspecto especial del lenguaje de programación: "La llamada 'type safety' va de la mano del hecho de que Rust impone restricciones al programador y no permite todo lo que éste quiere hacer. Sin embargo, a veces es necesario escribir una operación en el código que Rust no aceptaría debido a su seguridad de tipos", continúa el informático. "Aquí es donde entra en juego una característica especial de Rust: los programadores pueden marcar su código como 'inseguro' si quieren conseguir algo que contradiga las precauciones de seguridad del lenguaje de programación. Junto con colaboradores internacionales, entre ellos mi director de tesis Derek Dreyer, desarrollamos un marco teórico que nos permite demostrar que las afirmaciones de seguridad de Rust se mantienen a pesar de la posibilidad de escribir código "inseguro"", afirma Jung.

Esta prueba, llamada RustBelt, la complementa Ralf Jung con una herramienta llamada Miri, con la que se puede comprobar automáticamente que el código 'inseguro' de Rust cumple con importantes reglas de la especificación de Rust, un requisito básico para la corrección y seguridad de este código. "Mientras que RustBelt tuvo un gran éxito, sobre todo en los círculos académicos, Miri ya está establecida en la industria como herramienta para probar la seguridad de los programas escritos en Rust", explica Ralf Jung.

Por su disertación titulada "Comprensión y evolución del lenguaje de programación Rust". Ralf Jung ha recibido varios premios nacionales e internacionales. El trabajo de Jung recibió una de las dos "Menciones Honoríficas" del "Premio a la Disertación" de la "Association for Computing Machinery" (ACM). La ACM afirma: "A través del liderazgo de Jung y su compromiso activo con el grupo de trabajo de las Directrices de Código Inseguro de Rust, su trabajo ya ha tenido un profundo impacto en el diseño de Rust y ha sentado bases esenciales para su futuro". El premio ACM Dissertation Award se anuncia a nivel internacional para todo el campo de la informática, por lo que se considera uno de los premios más prestigiosos para las disertaciones de informática en todo el mundo.

También ha recibido el 'Doctoral Dissertation Award' de las 'European Joint Conferences on Theory & Practice of Software' (ETAPS), uno de los premios más importantes en el campo de la ciencia del software en Europa. También ha recibido la medalla Otto Hahn de la Sociedad Max Planck, que se concede anualmente por logros científicos especialmente destacados en relación con una disertación.

Más información