| Support | |
 |
 |
Fiabilidad y seguridad
Políticas de recursos.
Hemos continuado desarrollando analizadores estáticos que computan relaciones de recurrencias sobre la utilización de recursos de las aplicaciones, así como métodos matemáticos para derivar límites superiores e inferiores de estas relaciones de recurrencia. En concreto, hemos desarrollado una aproximación para inferir cotas superiores sobre los requisitos de memoria de programas al estilo Java, que es paramétrica con respecto a la noción de "vida de un objeto". Los resultados experimentales realizados sobre programas en código de bytes de Java ponen de manifiesto la utilidad y precisión de los análisis desarrollados. En un trabajo relacionado se han presentado los detalles técnicos e implementación de un comparador de expresiones de coste, que permite determinar si la ejecución de un programa se va a mantener dentro de unos límites determinados por el usuario.También hemos desarrollado un marco general para la verificación estática de propiedades que contempla propiedades globales no funcionales (tiempo de ejecución, memoria, energía, o recursos definidos por el usuario) como funciones de los tamaños de los datos de entrada. Un aspecto novedoso de este marco es que la comprobación estática genera respuestas que incluyen condiciones sobre la entrada en virtud de las cuales una especificación determinada puede ser demostrada o desmentida. Hemos implementado e integrado las técnicas de verificación desarrolladas en el sistema Ciao/CiaoPP.
Como complemento del trabajo anterior, y en conexión con el desarrollo de lenguajes de alto nivel para la definición de políticas de recursos, hemos desarrollado una herramienta de perfilado que asocia un coste a ciertos elementos del programa. Esta herramiente puede medir propiedades relacionadas con los recursos que afectan al rendimiento, proporcionando explicaciones para poder mejorar el rendimiento de los programas y permitiendo la detección automática de los procedimientos que son cuellos de botella del rendimiento.
En este contexto, también hay que destacar que Edison Mera ha defendido su tesis doctoral durante el período correspondiente al presente informe.
Seguridad basada en lenguajes.
Continuaremos desarrollando mecanismos que den soporte a la imposición de políticas flexibles y adaptables, así como mecanismos que permitan asegurar que dichas políticas se cumplen.Hemos trabajado en una versión avanzada de CertiCrypt, un entorno de certificación de primitivas criptográficas que usa el enfoque de seguridad basada en el lenguage. Hemos repasado y categorizado las técnicas de programación que se usaron en la prueba de seguridad del esquema de seguridad IND-CCA del esquema OAEO, la primera completa y mecanizada que se conoce. A su vez, CertiCrypt se ha utilizado en una formalización comprobada mediante ordenador de una teoría general de una clase de protocolos (protocolos Sigma) que tienen amplia aplicación en la criptografía. Asimismo, en el campo de la privacidad, hemos trabajado en la definición de lenguajes genéricos para definir políticas de privacidad tanto de proveedores de servicios como de usuarios de los mismos.
Seguridad basada en modelos.
Hemos extendido nuestros resultados sobre análisis de políticas de control de acceso basado en metamodelos, para analizar también políticas de control de uso y pretendemos desarrollar una metodología para el análisis de consistencia de las diferentes vistas del sistema con respecto a las políticas de seguridad y otros aspectos modelados por cada una de las vistas por separado.En concreto, hemos implementado la herramienta SSG, un entorno de desarrollo basado en modelos para interfaces gráficas con seguridad inteligente. SSG consta de varios plug-ins para Eclipse e incluye tres editores de modelos. Una componente fundamental de esta herramienta es un generador que hemos construido para obtener código MySQL a partir de expresiones OCL; hemos analizamos la eficiencia del código MySQL generado e implementado el generador en la herramienta MySQL4OCL.
En esta línea de investigación se ha dirigido un trabajo de fin de máster en el que se utiliza el lenguaje OCL sobre el metamodelo de Java para definir y ejecutar un conjunto no trivial y extensible de métricas sobre programas Java.
