N-GREENS SOFTWARE
NEXT-GENERATION ENERGY-EFFICIENT SECURE SOFTWARE
Descripción
Investigación
  Publicaciones
  Herramientas desarrolladas
Personal
Charlas & Eventos
Ofertas de empleo
Contacto
Programa Anterior
PROMESAS
PROMETIDOS
Comunidad de Madrid
mid

EU flag

Herramientas desarrolladas

Uno de los objetivos principales del Programa es el desarrollo y prefeccionamiento de herramientas que permitan cristalizar los avances del proyecto, desarrolando casos de estudios de alto impacto social y aprovechando la amplia red de colaboraciones industrialesdel Programa para maximizar la transferencia de tecnología.

La oferta de estas herramientas que el Programa pone a disposición de la comunidad científica, se plasma en el catálogo de las mismas:

  • Action-GUI: Es una metodología de desarrollo basada en modelos para aplicaciones web que garantiza la gestión segura de información. La herramienta incluye herramientas como editores para modelar los datos, la seguridad, y las interfaces gráficas, que son capaces de generar automáticamente aplicaciones web. El desarrollo y la comercialización de ActionGUI se lleva a cabo conjuntamente por el Instituto IMDEA Software y ETH Zurich, en los términos establecidos en un acuerdo firmado en diciembre de 2012.
  • Ciao: Es un sistema de programación multiparadigma con un entorno de desarrollo que incluye un sofisticado sistema (CiaoPP) para la optimización, y el análisis y verificación de un abanico muy amplio de propiedades funcionales y no funcionales. Ciao también dispone de un marco general de análisis del consumo de recursos, de gran relevancia para este proyecto. Recientemente hemos realizado experimentos preliminares para la estimación del consumo de energía con resultados muy alentadores que indican que Ciao es una buena infraestructura para el desarrollo de software conscientes del consumo de energía.
  • DES: Es un sistema de bases de datos deductivas (BDD) gratuito, de código abierto, interactivo y portable. DES soporta los lenguajes de consulta Datalog, SQL y álgebra relacional. DES es un sistema muy utilizado internacionalmente (más de 48K descargas) en enseñanza e investigación, incluyendo estudios de fallos de seguridad en Mozilla Firefox, optimización de consultas con vistas materializadas y modelos de minería de datos, toma de decisiones cuantitativa en ingeniería del software, comprobación al vuelo de la integridad de los metadatos en sistemas de ficheros, ontologías y web semántica.
  • EasyCrypt: Es una plataforma para analizar la seguridad de construcciones criptográficas, basada en utilizar análisis de lenguajes de programación para manejar la complejidad y rigor del análisis de construcciones criptográficas. EasyCrypt ha ayudado a identificar errores en análisis previos de estándares muy difundidos, como PKCS.
  • Leap: Es un sistema moderno de verificación de sistemas parametrizados concurrentes que manipulan tipos de datos complejos en memoria dinámica. Leap está basado en la separación entre el razonamiento sobre trazas de ejecución y sobre los datos compartidos, para lo cual se usan procedimientos de decisión específicos para estos datos.
  • Maude: Es un lenguaje de propósito general de alto nivel y un sistema de alto rendimiento que soporta lógica ecuacional y de reescritura para una gama amplia de aplicaciones, incluyendo sistemas ciberfísicos y sistemas con propiedades críticas de seguridad. Las versiones más recientes incluyen soporte para unificación módulo axiomas, sobre cuya base se han implementado versiones limitadas de "narrowing", pero que han probado su utilidad para el análisis de protocolos criptográficos con propiedades algebraicas.
  • Smack: Un obstáculo importante para la transferencia de la investigación en fiabilidad de software es lo costoso de desarrollar una infraestructura que soporte software industrial en toda su complejidad. SMACK persigue reducir drásticamente estos costes a través de la conexión entre el lenguaje intermedio de compilación de LLVM y lenguajes intermedios de verificación como Boogie y Why3, lo que permite reusar esfuerzos para muchos lenguajes fuente diferentes como C/C++, Haskell o Erlang.
  • Jsongen: Es una librería para la generación aleatoria de valores JSON a partir de un esquema (tipo) de los mismos. Actualmente, las implementaciones RESTful (Representational State Transfer) de servicios web están primando sobre opciones más "pesadas" (WS*/SOAP) siendo JSON el lenguaje icono para la representación de la información. El testing de dichos servicios pasa por disponer de masivas cantidades de datos que poder enviar y recibir del servidor. Entre las funcionalidades de la librería estarán: generar valores JSON aleatorios a partir de una descripción de los mismos (ej. utilizando JSON Schema), validar dichos datos, o introducir mutaciones en los datos.
  • Umerl: Es una aplicación para ejecutar y verificar sistemas especificados en UML. Las especificaciones son, esencialmente, redes de máquinas de estado que se comunican asíncronamente. El objetivo de Umerl es anticipar errores en las especificaciones y el diseño de sistemas críticos antes de su implementación. Para ello Umerl introduce una semántica precisa, no ambigua, y al mismo tiempo amigable con la filosofía UML. La aplicación consiste en un intérprete implementado en Erlang capaz de ejecutar un sistema descrito en UML mediante diagramas de estados, diagramas de clase y diagramas de objeto. Dicha ejecución es validada mediante testing dirigido por propiedades y también verificada utilizando McErlang.