Buscan un "software perfecto" para evitar grandes desastres humanos, materiales o económicos

València

La Universitat Politècnica de València (UPV), como miembro del Instituto Valenciano de Inteligencia Artificial (VRAIN), participa en el proyecto EuroProofNet, una red de investigación europea sobre pruebas digitales cuyo objetivo es contribuir a lograr el software libre de errores. La ausencia de errores es la gran quimera de la industria del software. Desde las aplicaciones para móviles hasta sectores críticos como el control del tráfico o las transacciones bancarias, garantizar la ausencia de errores de la arquitectura informática es cada vez más necesario.

La puesta en marcha de este grupo de investigación se enmarca dentro de una acción COST (European Cooperation in Science and Technology) sobre pruebas formales de software que persigue poner a Europa al frente del liderazgo de la verificación formal.

Tal y como destaca Alicia Villanueva, investigadora del Instituto VRAIN de la UPV, actualmente existe software muy seguro "porque pasa por un análisis y verificación formal muy exigente, y estas pruebas son claves, porque el menor de los fallos puede provocar grandes desastres humanos, materiales o económicos. Y lo son a todos los niveles".

Herramientas más accesibles

“Por ejemplo, a veces no somos conscientes de la importancia de que las 'apps' de nuestros móviles sean verificadas. Muchas de ellas gestionan nuestros datos, nuestras cuentas, por lo que cualquier vulnerabilidad puede afectar tanto a los usuarios como a las propias empresas desarrolladoras".

"Por eso es importante intentar avanzar no solo en el desarrollo de las propias técnicas, sino también en hacer las herramientas más accesibles". Esta experta llama la atención sobre la necesidad de prestar atención y exigir seguridad en todos los ámbitos.

Únete al canal de WhatsApp de la SER

"Hoy en día no solo son críticos los sistemas de control aeronáuticos, ferroviarios, etcétera, que tienen presupuestos millonarios y para los que ya hemos aceptado la necesidad de garantizar su corrección, sino que haciendo más accesibles las herramientas de verificación formal podremos ayudar a mejorar la seguridad y calidad de cualquier sistema software cuyos fallos puedan condicionar nuestras vidas”, apunta Villanueva.

La red cuenta con más de 200 investigadores de 30 países, tanto de la Unión Europea como de fuera de ella, e incluye seis grupos de trabajo, cada uno de ellos especializado en un área concreta. El equipo de VRAIN-UPV lidera el grupo que trabaja en la verificación de programas.

“En este grupo, lo que tratamos de mejorar son las técnicas de verificación formal que a su vez hacen uso de los sistemas de prueba formales.

La importancia de la verificación

La principal característica de la verificación formal es que es capaz de garantizar que una propiedad se cumple para cualquier posible ejecución, contribuyendo así a la seguridad del software”, explica Alicia Villanueva.

"Actualmente existen multitud de herramientas de verificación eficaces -señala esta experta- pero muchas veces se especializan en resolver un tipo de problema concreto.

En este contexto EuroProofNet tiene dos grandes objetivos: por un lado, mejorar las interoperabilidad y usabilidad de los sistemas de prueba formales, para así contribuir al avance de las herramientas de verificación que hacen uso de ellos y, por otro, mejorar la interoperabilidad entre sistemas de verificación para aprovechar lo mejor de cada técnica".

“Todo ello contribuirá a garantizar la seguridad de los programas informáticos”, remarca Alicia Villanueva.

Además de los objetivos puramente científicos, EuroProofNet pretende construir una red de investigadores que fomente la colaboración y ayude a avanzar en este sentido. La red desarrollará sus actividades hasta octubre de 2025.

Evitar que los hackers se aprovechen de errores

Con respecto a la seguridad frente a ataques, los hackers suelen aprovechar errores en el software como puede ser una comprobación mal hecha o el uso de librerías o protocolos que tienen fallos conocidos (muchos descubiertos o confirmados gracias a la verificación formal) y que abren la puerta a los intrusos.

Otras veces consiguen entrar por un error manual de configuración o a través de la cuenta de algún empleado (como parece que ha sido el caso del reciente caso anunciado por Microsoft) cuya contraseña se ha visto expuesta por cualquier motivo. Normalmente el objetivo de estos ataques son las grandes compañías que pierden el control de sus sistemas o ven comprometidos los datos de sus clientes (a veces nuestros datos, incluso nuestras contraseñas).

Hay acciones muy sencillas que podemos hacer como usuarios para limitar los efectos de este tipo de ataques. Por ejemplo, podemos evitar usar la contraseña que da acceso a los sistemas de nuestro trabajo en otros sitios web o gestores de correo, por si se viera expuesta.

También podemos prestar atención a las direcciones web que nos llegan en un correo: sabemos cuál es el dominio (el inicio de la dirección web, normalmente la página principal) de empresas como correos, nuestro banco o nuestro seguro.

Si recibimos un correo solicitándonos nuestra contraseña o que descarguemos un fichero, al pasar el ratón por encima del enlace podemos ver la dirección web antes de acceder a ella. Si esa dirección no está el dominio o está al final de la url, debemos sospechar y ni siquiera pinchar en ese enlace. Así evitaremos la propagación de virus y aplicaciones que capturan nuestras contraseñas cuando las usamos.