Especificación de Scilla en Maude

Abstract

Este trabajo busca proporcionar una especificación formal al lenguaje de contratos inteligentes Scilla mediante el lenguaje Maude, para así poder ejecutar contratos reales siempre que estén escritos adecuadamente y realizar un análisis para detectar partes de código muerto, es decir, variables que no van a ser usadas en ningún momento. Para llevar a cabo esta implementación, se ha tenido que realizar una transformación previa del archivo de entrada por ciertas limitaciones que tiene Maude, se han creado dos gramáticas: la primera, muy parecida a la sintaxis de Scilla, se utiliza para analizar sintácticamente el archivo de entrada; por su lado, la segunda gramática es más funcional y se utliza para trabajar internamente. Para la descripción de la semántica se ha creado una memoria para poder almacenar las variables con los valores y el nombre, entradas y cuerpo de los procedimientos, funciones y transiciones de Scilla, y distintas reglas de reescritura que permiten actualizar esos datos en la memoria y ejecutar las operaciones. También, el usuario podrá interactuar con el sistema por medio de la entrada/salida, donde puede introducir un contrato válido, indicar si quiere analizarlo o ejecutarlo y en el caso de que se quiera ejecutar, introducir los valores necesarios para ello. También recibirá respuesta por parte del sistema, en el caso del análisis, indicando si el contrato es correcto o si tiene partes que no se usan, mostrando cuáles son y a qué función, transición o procedimiento corresponde y, en el caso de la ejecución, devolviendo el estado de las variables que son globales y además, la información de la transición ejecutada. Por último, se busca también que el análisis sea escalable para no solo analizar contratos escritos en Scilla, sino en cualquier otro lenguaje. Para ello, se ha parametrizado el código, es decir, en vez de poner la sintaxis concreta de las partes que se quieren analizar de Scilla dentro del código que realiza el análisis, se especifica aparte y se pasa como parámetro.

The present project seeks to provide a formal specification to the Scilla smart contract language using the Maude language, in order to be able to execute real contracts, as long as they are properly written, and to perform an analysis in order to detect parts of dead code, specifically variables that are not going to be used at any time. In order to implement it, the input file had to be previously converted due to certain limitations of Maude. Thus, two grammars have been created. On the one hand, the first one, very similar to Scilla syntax, is used to syntactically analyze the input file. On the other hand, the second grammar is more functional and is used to work internally. For the description of the semantics, a memory has been created to save the variables that include the values, the names, the entries and the body of Scilla procedures, functions and transitions, as well as different rewrite-rules that allow updating these data in the memory and implementing the operations. In addition, the users can interact with the system through input/output, where they can enter a valid contract, indicate whether they want to analyze or execute it and, in that case, enter the necessary values for it. The users will also receive a response from the system, in the case of analysis, indicating if the contract is correct or if it has modules that are not used, showing which ones are and to which function, transition or procedure they correspond, and, in the case of execution, returning the status of the variables that are global, as well as the information of the transition executed. Finally, the analysis is also intended to be scalable to not only analyze contracts written in Scilla language, but also in any other language. For this purpose, the code has been parameterized, that is, instead of introducing the specific syntax of the Scilla modules to be analyzed within the code that performs the analysis, it is specified separately and passed as a parameter.