RT Generic
T1 Semántica de WebAssembly en Maude
T1 Semantics of WebAssembly in Maude
A1 Morales Palacios, Rafael
AB 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 WebAssemblyin 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.
AB 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
YR 2025
FD 2025
LK https://hdl.handle.net/20.500.14352/125016
UL https://hdl.handle.net/20.500.14352/125016
LA eng
NO Trabajo de Fin de Máster en Métodos Formales en Ingeniería Informática, Facultad de Informática UCM, Departamento de Sistemas Informáticos y Computación, Curso 2024/2025
DS Docta Complutense
RD 18 dic 2025