Providing formal semantics for Solidity to allow its verification

Abstract

Whilst the number of programming languages continuously increases, along with their multiple applications, the need of guaranteeing correction or predicting the outcome of a certain program arises. Due to the lack of information that is often available in the official documentation of the languages, formal methods seem a powerful tool in this sense. Thanks to program verification using formal semantics we can abstract the behaviour of an instruction using mathematical notation. In this work we will study Solidity, a language used to create the so-called smart contracts in the Ethereum platform. Our goal is to study the state-of-the-art semantics in this topic, to ultimately suggest our own, with the aim of covering what we believe has not been covered yet, and to propose modifications to the rules that we have found rather imprecise. We have decided to pay special attention to how values are updated and retrieved from the storage, which is one on the four data locations Solidity makes use of. Lastly, it has been our goal to propose semantics that are executable in languages like K or Maude. For this reason, we have also coded several Maude modules which can be helpful when verifying a contract using this language.

En un contexto en el cual el número de lenguajes de programación cada vez es más elevado, y su uso se extiende a un mayor número de ámbitos, aparece la necesidad de asegurar la corrección o de determinar el resultado de ciertos programas. Debido a la falta de información concreta que muchas veces encontramos en la documentación oficial de los lenguajes, surgen técnicas como la verificación de programas a través de semánticas formales, que permiten modelizar mediante abstracciones matemáticas el funcionamiento de las instrucciones. En este trabajo estudiaremos el lenguaje Solidity, utilizado para crear los llamados smart contracts en la plataforma Ethereum. Nuestro objetivo es estudiar qué propuestas de semánticas se han hecho, para posteriormente aportar la nuestra, que tratará de rellenar y corregir ciertos huecos e imprecisiones que hayamos podido encontrar en la literatura consultada. En nuestro caso, presentamos una semántica centrada sobre todo en la obtención y actualización de valores en storage, una de las cuatro memorias que utiliza Ethereum. Por último, el objetivo último de este trabajo es el ofrecer una semántica que sea implementable en lenguajes como K o Maude. En nuestro caso, hemos desarrollado diferentes módulos en Maude que pueden servir como base a la hora de realizar una verificación de un contrato en este lenguaje.