Semántica de WebAssembly en Maude

Abstract

WebAssembly (Wasm) is a low-level programming language designed, at first, to improve the performance of web applications. Through the years, it has gained popularity in several other fields, including Internet of Things, edge computing, and smart contracts.

A distinctive feature of this language is that it has been formally defined with a set of semantic and validation rules for its instructions. In this Master’s thesis, we propose a formalization of the semantics of WebAssembly in Maude, an executable specification language based on rewriting logic. This formalization represents WebAssembly programs and environment as terms and the exection of its instructions as rewrite rules, following the semantic rules of the original specification.

In addition, the semantics can be used as an interpreter of the language, which we have verified that behaves like the official interpreter using differential testing. Finally, we show how it can be used to verify properties on WebAssembly programs.

WebAssembly (Wasm) es un lenguaje de programación de bajo nivel diseñado, en un principio, para mejorar el rendimiento de aplicaciones web. A lo largo de los años, ha ganado popularidad en diferentes campos, incluyendo el Internet de las Cosas, la computación frontera y los contratos inteligentes. Una característica singular de este lenguaje ha sido definido formalmente con un conjunto de reglas semánticas y de validación para sus instrucciones.

En este Trabajo de Fin de Máster, desarrollamos una formalización de la semántica de WebAssembly en Maude, un lenguaje de especificación ejecutable basado en la lógica de reescritura. Esta formalización representa los programas y el entorno de WebAssembly como términos y la ejecución de sus instrucciones como reglas de reescritura, siguiendo las reglas semánticas de la especificación original. Además, la semántica se puede utilizar como un intérprete del lenguaje, que hemos comprobado que se comporta como el intérprete oficial mediante testing diferencial. Finalmente, mostramos cómo puede utilizarse para verificar propiedades sobre programas de WebAssembly