MÉTODOS FORMALES ESCALABLES PARA APLICACIONES REALES

2022

AGENCIA ESTATAL DE INVESTIGACION

INV. COMPETITIVA PROYECTOS

Escobar Román Santiago

Dada la ubicuidad de los sistemas informáticos en aplicaciones cuya seguridad es crítica, es cada vez más importante para la sociedad asegurar que dichos sistemas se comportan correctamente. El proyecto SFERA aplica métodos formales para garantizar, a través de razonamientos formales, la correcta ejecución de los sistemas informáticos, centrándose así en el área de prioridad "mundo digital, industria, espacio y defensa'' y, en particular, en su línea estratégica "modelización y análisis matemático y nuevas soluciones matemáticas para ciencia y tecnología''. Una ventaja de los métodos formales es que son capaces de proporcionar garantías matemáticas sobre la protección y seguridad de los métodos analizados módulo la precisión de los métodos formales utilizados, y también de la corrección de los razonamientos usados en la implementación. Sin embargo, dependiendo de la precisión y la escalabilidad de las técnicas utilizadas, no siempre es posible obtener un resultado a partir de ellas. Este es precisamente el núcleo principal del proyecto SFERA: pasar de un ámbito general --pero no siempre preciso y eficiente-- a aproximaciones más precisas y escalables. Actualmente, y sin menospreciar los esfuerzos realizados (incluyendo nuestros proyectos previos), la aplicación de métodos formales a sistemas del mundo real y de tamaño grande ha estado limitado a pocos casos y en dominios específicos. El proyecto SFERA está enfocado a investigar y mejorar la escalabilidad y precisión, dentro de sus cuatro objetivos científicos, y así lograr avances significativos dentro de los métodos formales, con especial atención en la aplicabilidad de las técnicas desarrolladas para asegurar la fiabilidad y eficiencia en aplicaciones a gran escala. Se utilizará verificación, testeo, análisis y optimización sobre un amplio rango de sistemas, desde "smart contracts" que se ejecutan sobre el "blockchain", hasta protocolos de seguridad y aplicaciones dirigidas por datos. Para algunos de estos propósitos, el uso de resolutores para problemas relacionados con SAT será esencial. Esperamos conseguir las siguientes contribuciones dentro de nuestros cuatro objetivos: (1) desarrollar técnicas escalables y herramientas para resolver problemas que sean relevantes para la industria, (2) avanzar en la síntesis de propiedades complejas, que surgen en el contexto de las aplicaciones reales, (3) mejorar las técnicas de métodos formales para su mejor escalabilidad y (4) desarrollar técnicas e instrumentos para medidas y supervisión en inteligencia artificial, aprendizaje automático y testeo. SFERA es un proyecto coordinado con cuatro grupos de investigación de UCM, UPV, UPC y UPM. Los conocimientos complementarios de estos grupos son fundamentales para conseguir los objetivos del proyecto: UPV tiene amplia experiencia en el área de los lenguajes de programación, a nivel semántico y de implementación. UCM tiene más experiencia en la verificación, testeo y técnicas de análisis de programas. UPC investiga en la teoría de herramientas deductivas y en aplicaciones industriales. UPM tiene una experiencia relevante en la certificación, análisis incremental, sistemas escalables, y en la transferencia tecnológica a la industria. Los grupos han colaborado con investigadores internacionales de reconocido prestigio y en la actualidad trabajan de forma activa con empresas en temas muy relacionados con el proyecto SFERA.