Resultados de investigación
El investigador del Instituto IMDEA Software, Manuel Hermenegildo, imparte la conferencia invitada inaugural del 27th Static Analysis Symposium (SAS'20), sobre el trabajo en “Cost Analysis of Smart Contracts via Parametric Resource Analysis”, en el que participan también: Víctor Pérez, Maximiliano Klemen, Pedro López y José Francisco Morales.
Esta línea de trabajo está motivada por el hecho de que, en las cadenas de bloques (blockchains), la ejecución de contratos y el almacenamiento se replican a través de un gran número de nodos, lo que hace que el consumo de recursos sea una preocupación importante. Los pocos analizadores de coste que existen para contratos inteligentes son para plataformas y lenguajes específicos. Sin embargo, las plataformas de cadenas de bloques presentan una variabilidad significativa, también a lo largo del tiempo.
El Análisis de Recursos Paramétricos (también conocido como Análisis de Recursos Definidos por el Usuario) es un enfoque genérico, propuesto por el equipo del Instituto IMDEA Software, para desarrollar analizadores que infieren límites seguros en diferentes recursos y con diferentes modelos de recursos. Manuel Hermenegildo comenta en la conferencia que el Análisis Paramétrico de Recursos explora su aplicación a la inferencia estática de los límites de consumo de gas y almacenamiento para contratos inteligentes, e informa sobre un caso de estudio concreto: el desarrollo de un analizador para la plataforma Tezos y su lenguaje Michelson. Los resultados muestran que el enfoque es un método efectivo para el rápido desarrollo y mantenimiento de analizadores de coste para contratos inteligentes.
La propuesta de Análisis de Recursos Paramétricos fue premiado con el 10 year Test-of-Time Award en la 2017 International Conference on Logic Programming, la conferencia por excelencia en el área.
El marco CiaoPP, desarrollado por el Instituto IMDEA Software, implementa este enfoque y permite su aplicación a diferentes lenguajes de programación, mediante la traducción a una representación intermedia basada en cláusulas de Horn.
La serie de congresos Static Analysis Symposium (SAS) es el foro principal para la presentación de avances teóricos, prácticos y de aplicación en el área de análisis estático de programas. Esta edición de SAS está co-ubicada con SPLASH'20 en un formato online, coordinado desde Chicago, EEUU, desde el 18 al 20 de noviembre de 2020. SPLASH abarca todos los aspectos de la construcción y entrega de software, para convertirlo en la principal conferencia sobre las aplicaciones de los lenguajes de programación - en la intersección de los lenguajes de programación y la ingeniería de software.
Este trabajo se ha llevado a cabo en el contexto de la colaboración de la fundación Tezos y los laboratorios Nomadic con el Instituto de Software IMDEA.
