Análisis de contratos inteligentes usando Cláusulas de Horn

Pérez Carrasco, Víctor (2020). Análisis de contratos inteligentes usando Cláusulas de Horn. Proyecto Fin de Carrera / Trabajo Fin de Grado, E.T.S. de Ingenieros Informáticos (UPM), Madrid, España.

Description

Title: Análisis de contratos inteligentes usando Cláusulas de Horn
Author/s:
  • Pérez Carrasco, Víctor
Contributor/s:
  • Hermenegildo Salinas, Manuel Vicente
Item Type: Final Project
Degree: Grado en Ingeniería Informática
Date: 7 June 2020
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (358kB) | Preview

Abstract

En software crítico, es común la necesidad de demostrar que las aplicaciones se atienen a unas especificaciones sobre el consumo de recursos. Para ello, el análisis estático se postula como una solución claramente superior al testing, ya que este último se limita a probar la no conformancia mediante la búsqueda de un caso que no cumpla con las condiciones, mientras que solo el primero puede asegurar que las especificaciones se respetan para un conjunto infinito de posibles entradas. En este trabajo, nos centramos en el análisis de un tipo de software crítico cuya popularidad ha crecido considerablemente en los últimos años: los contratos inteligentes. La propia naturaleza de los contratos inteligentes y de las blockchain hace que el análisis del consumo de recursos en estos sea de gran importancia. El alto factor de replicación de estos programas en los nodos de las plataformas distribuidas hace que hasta la operación más sencilla vea su coste computacional multiplicado y que el espacio de almacenamiento requerido por estos crezca vertiginosamente. Esta situación, unida a la mutabilidad y variabilidad de las plataformas en cuanto a lenguajes utilizados y modelos de coste empleados, empuja a pensar que una aproximación genérica y configurable a este problema sea una opción interesante. Esto contrasta con las soluciones propuestas anteriormente que son más específicas para un lenguaje de contratos o una plataforma dados. Siguiendo esta línea, en este trabajo presentamos un enfoque flexible y viable al análisis estático de contratos inteligentes, particularizado a la plataforma Tezos. Para ello implementamos un traductor de Michelson a Cláusulas de Horn, las cuales se analizan con la herramienta CiaoPP. El análisis realizado se enfoca principalmente en estimar el consumo de gas, un recurso virtual que refleja el tiempo de ejecución de un programa. Dicho análisis se apoya en un modelo de coste que hemos expresado en un lenguaje de aserciones, y que recoge la información en términos de consumo de recursos de las distintas instrucciones presentes en el lenguaje Michelson. De este modo, se presenta la posibilidad de realizar un análisis de recursos altamente configurable que se adapte a las modificaciones que pueda sufrir la plataforma a estudiar a lo largo del tiempo. Presentamos resultados experimentales del análisis estático de contratos inteligentes obtenidos con la técnica propuesta que muestran que la solución es factible, y puede ser precisa y eficiente. Estos resultados son alentadores, y sugieren que esta técnica es una vía prometedora para continuar explorando en el futuro.---ABSTRACT---In critical software, it is usually needed to ensure the conformance of applications with respect to specifications that constrain resource usage. In order to achieve this, static analysis stands as a clearly superior solution compared to testing, as the latter is only capable of proving that a program does not meet the necessary conditions by searching for a non-compliant case, whereas only the former can assure that specifications are complied with for an infinite set of possible inputs. In this work, we will focus on the analysis of a kind of critical software which is becoming increasingly popular in the last few years: smart contracts. The very nature of smart contracts and blockchain makes resource analysis on these of great importance. The high replication factor presented by these programs in distributed platform nodes leads to the multiplication of the computational cost of running even the simplest operation and the rapid growing of the consumed storage space. This situation, combined with the mutability and variability that these platforms present in terms of languages and cost models, compels one to think that a generic and configurable approximation to this problem is an interesting option. This is in contrast with previous approaches that are more specific for a contract language or platform. Following this line, in this work we present a flexible approach to the static analysis of smart contracts, using the Tezos platform as the concrete case of application. To this end, we have implemented a Michelson to Horn Clause translator and run CiaoPP’s static resource analysis on Tezos smart contracts represented this way. The analysis focuses on analyzing gas consumption, a virtual resource which reflects a program’s execution time. Such analysis relies on a cost model that we have expressed using an assertion language, which represents the resource consumption for each Michelson instruction. This way, it is possible to perform a highly configurable resource analysis, capable of adapting to possible changes that the platform might suffer over time. We present experimental results on the static analysis of smart contracts obtained using the proposed approach which show that the approach is feasible, and can be accurate and efficient. These results are encouraging, and suggest that the approach is indeed a promising avenue for future research.

More information

Item ID: 62948
DC Identifier: http://oa.upm.es/62948/
OAI Identifier: oai:oa.upm.es:62948
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 09 Jul 2020 09:00
Last Modified: 09 Jul 2020 09:00
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM