Explora I+D+i UPV

Volver atrás Servicio de I+D

Verificación y certificación automática de propiedades de seguridad y confianza en protocolos de comunicaciones y código móvil

Institut Universitari Valencià d'investigació en Intel·ligència Artificial

Imprimir
Compartir
¿Quieres contarnos tu reto? Pincha aquí y te ayudamos a encontrar una solución
Los productos software suelen carecer de garantía industrial de buen funcionamiento, a diferencia de los productos hardware habituales en informática. Este hecho, asumido por la mayoría de los usuarios, es totalmente inaceptable en aquellos dominios de aplicación críticos, donde se establecen propiedades explícitas de seguridad (safety) y de confianza (security). Se entiende por propiedades de confianza (security) aquellas donde se protege al sistema del entorno, p.ej. ataques y brechas de seguridad, y por propiedades de seguridad (safety) aquellas donde se protege al entorno del sistema, por ejemplo. filtrado accidental de información, mala gestión de recursos compartidos, etc. Se han desarrollado técnicas para el análisis, verificación y certificación de sistemas concurrentes y/o reactivos, es decir, sistemas con un comportamiento indeterminista y/o infinito, y técnicas para sistemas software en general, es decir, sistemas (posiblemente deterministas o finitos) donde las acciones tomadas a lo largo del tiempo pueden no ser relevantes, a diferencia de los concurrentes, sino ciertas propiedades satisfechas en todo momento (invariantes) o satisfechas en algún punto especifico de su ejecucion (propiedades funcionales). En concreto, ofrecemos herramientas para: el análisis y verificación de propiedades de confianza (security) en protocolos de comunicaciones criptográficos (por ejemplo, Diffie-Hellman); la verificación y certificación de propiedades de seguridad (safety) en código móvil (por ejemplo, Java) y la verificación de propiedades en sistemas software genéricos (por ejemplo, mala gestión de recursos compartidos).
Responsable científico

Escobar Román Santiago

Participantes

Escobar Román Santiago, Alba Castro Mauricio Fernando, Alpuente Frasnedo María, Santiago Pinazo Sonia

Aplicaciones

  • Verificación de protocolos criptográficos.
  • Análisis de no filtrado y desclasificación de información secreta.

Ventajas técnicas

  • Verificación de propiedades de seguridad en protocolos de comunicaciones y verificación de propiedades de comportamiento en programas Java. Si el protocolo o aplicación no cumple las propiedades proporcionamos un contra ejemplo, para que dicho protocolo o aplicación pueda ser reparado.

Beneficios que aporta

  • Hemos desarrollado la única técnica del mercado aplicado al lenguaje Java al completo.
  • Otras técnicas utilizan lenguajes de programación de juguete mientras que nosotros analizamos Java 1.4

Experiencia relevante

  • El grupo ELP, creado en 1989, está identificado en el registro de grupos de investigacion consolidados de la Generalitat Valenciana desde Octubre de 2000 (clave GR-00143). La actividad del grupo se ha relacionado principalmente con los lenguajes de programación multiparadigma y los métodos rigurosos para el desarrollo del software, focalizando en la programación basada en reglas y el uso de técnicas de interpretación abstracta y técnicas de transformación para la optimización de la ejecución de los programas. Los lenguajes basados en reglas han sido también la base para la programación inductiva y para la representación de modelos complejos, pero a su vez, comprensibles, resultantes de la extracción de conocimiento a partir de datos (minería de datos). El grupo ELP ha participado en más de 30 proyectos competitivos financiados con fondos europeos, nacionales y comunitarios. Su actividad investigadora se ha desarrollado a menudo en conexión con grupos afines radicados en universidades extranjeras, incluyendo Alemania (RWTH Aachen, U. de Kiel), Australia (Monash U.), Austria (Technische Universitat Wien), Estados Unidos (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), Francia (-'Ecole Polytechnique, U. Grenoble, U. Niza, U. de Paris Sud), Italia (U. di Pisa, U. di Siena, U. di Udine) y Reino Unido (U. Bristol). El grupo ha participado en diversos proyectos con empresas donde se ha transferido el conocimiento del grupo o se ha desarrollado tecnología específica. El abanico de sectores en los que el grupo ha trabajado incluye, lógicamente, empresas de informática y consultoría, pero también empresas que van desde del ámbito de la distribución a la gestión hospitalaria. // The group ELP, created in 1989, was recognized as a consolidated group of the Valencian Government in October 2000 (reference GR-00143). The group's activities have mainly focused on multi-paradigm programming languages and rigurous methods for software development, with particular focus on rule--based programming, and the use of abstract interpretation and program transformation techniques for the optimization of program execution. Rule-based languages have been also used for inductive programming and complex model representation that are also comprehensible as a result of knowledge discovering (data mining). The ELP group has participated in more than 30 competitive research projects funded by the EU, the Spanish Research Funding Agency, and other European foundations. The group keeps a good record of international collaborations. Including Germany (RWTH Aachen, U. Kiel), Australia (Monash U.), Austria (Technische Universit-"at Wien), USA (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), France (-'Ecole Polytechnique, U. Grenoble, U. Niza, U. Paris Sud), Italy (U. di Pisa, U. di Siena, U. di Udine) and UK (U. Bristol). The Group also keeps a good record of collaboration with industry, including IT companies as well as hospital management and distribution companies.