Herramientas desarrolladas

Desarrollo y distribución de herramientas software.

El programa BLOQUES-CM transferirá parte de sus resultados científicos en forma de herramientas software.

A continuación se describen las herramientas existentes más destacadas en las que trabajaremos en el contexto del programa BLOQUESCM indicando su relación con los objetivos.

La oferta de las herramientas que el Programa pone a disposición de la comunidad científica, son:

• AVClass (https://github.com/malicialab/avclass) (Objetivo 1): AVClass es una herramienta de clasificación y etiquetado de ejecutables maliciosos (malware). Toma como entrada la lista de etiquetas asignadas al ejecutable por un alto número de motores antivirus (obtenidas de aplicaciones Web como VirusTotal) e identifica el nombre de la familia del ejecutable más usado por los antivirus junto con un factor de confianza. AVClass cuenta con 119 estrellas en GitHub (Julio 2018).
• FCSL (https://software.imdea.org/fcsl/) (Objetivo 2): Finegrained Concurrent Separation Logic (FCSL) es el primer entorno completamente formalizado para la verificación mecanizada de la corrección funcional de programas concurrentes de grano fino. Está implementada en un DSL en Coq y es suficientemente potente como para razonar sobre funciones de orden superior y arranque local de hilos de ejecución. FCSL posibilita la construcción de pruebas sobre librerías concurrentes de manera local y composicional, permitiendo la escalabilidad y la reutilización: las librerías sólo necesitan ser verificadas una vez y sus especificaciones pueden reusarse para razonamientos en el lado del cliente..
• DES (http://des.sourceforge.net) (Objetivo 3): 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, cálculos relacionales y álgebra relacional. DES es un sistema muy utilizado internacionalmente (más de 73K 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. Además de mejorar la robustez y cercanía al usuario de DES, trabajaremos entre otros aspectos en un entorno de desarrollo online, avances en lógica difusa, análisis de consultas para r realimentación semántica, y el uso de Datalog como lenguaje de especificación de alto nivel para smart contracts..
• Leap (https://github.com/imdeasoftware/leap (Objetivo 3): LEAP es un demostrador de teoremas que permite la verificación formal de propiedades temporales (tanto de seguridad como de vivacidad) de programas parametrizados concurrentes. LEAP está diseñado para analizar programas que manipulan tipos de datos concurrentes en el heap y cuya memoria durante la ejecución puede crecer sin límite. Dado un programa y una especificación, LEAP genera automáticamente una colección de condiciones de verificación. Asimismo, implementa procedimientos de decisión para un conjunto de teorías, como listas, skiplists, arrays, conjuntos, etc. y combinaciones de las mismas. Estas características convierten a LEAP en una base ideal para crear herramientas de generación interactiva de demostraciones para smart contracts..
• Ciao (http://ciaolang.org) (Objetivo 4): Es un sistema de programación multiparadigma con un entorno de desarrollo que incluye un sofisticado sistema (CiaoPP) para la optimización, el análisis y verificación de un abanico muy amplio de propiedades funcionales y no funcionales. El sistema proporciona soporte para el proceso de diferentes lenguajes de programación y representaciones de bajo nivel (tales como LLVM o ensamblador) mediante una transformación a un lenguaje intermedio basado en cláusulas de Horn. Ciao dispone de un marco general de análisis que ha sido especializado con éxito para inferir el consumo de varios recursos, tales como energía y tiempo de ejecución, de programas en diferentes representaciones (por ejemplo programas lógicos con restricciones y funcionales, programas Java, C, LLVM, ensamblador, etc.). Dichas características son de gran relevancia para este programa, en el que desarrollaremos las adaptaciones y transformaciones necesarias para analizar smart contracts en algunos de los diferentes lenguajes utilizados en las plataformas blockchain. Además, mejoraremos la robustez y escalabilidad de los motores de análisis para procesar aplicaciones reales en dichas plataformas, mediante el desarrollo de técnicas de análisis modular e incremental. Asimismo, mejoraremos una serie de técnicas instrumentales para el análisis de recursos, tales como resolutores de ecuaciones de recurrencia avanzados, y análisis del tamaño de datos.
• Maude (maude.cs.uiuc.edu) (Objetivo 4): Es un lenguaje de propósito general de alto nivel y un sistema de alto rendimiento que soporta computación lógica ecuacional y de reescritura, así como unificación y narrowing módulo axiomas. Estas características, unidas a sus potentes herramientas de verificación como comprobadores de modelos, demostradores de teoremas y analizadores de terminación, entre otros, han permitido estudiar una amplia gama de aplicaciones, incluyendo sistemas con propiedades críticas de seguridad, sistemas ciberfísicos y en tiempo real y protocolos criptográficos. Es asimismo un potente marco semántico y de metaprogramación que permite la definición y análisis de otros lenguajes de programación y de los programas escritos en ellos, demostrando su potencia incluso frente a compiladores como gcc en tests de estrés de C. Estas características hacen de Maude un marco idóneo para definir lenguajes de programación cuyos programas supongan un riesgo físico o económico y precisen, por tanto, estar formalmente verificados.

Es importante resaltar que todas estas herramientas están disponibles como software libre, con lo cual se cierra el círculo que revierte a la sociedad los recursos destinados a la investigación, sin que esto elimine la posibilidad de que versiones de las mismas puedan emplearse como fundación para el arranque de empresas de base tecnológica. Además durante la ejecución del programa se desarrollarán nuevas herramientas de las cuales también se espera que se conviertan en software libre o que constituyan la base de una posible comercialización.