Verification and Certification of EVM Optimizations

Abstract

The optimization of Ethereum Virtual Machine (EVM) bytecode presents unique challenges and opportunities due to its distinct requirements, including considerations such as execution cost and compiled binary size. Despite its potential benefits, optimization in this realm remains limited, primarily due to the high stakes associated with EVM programs, or smart contracts, where even minor errors can result in significant financial losses. To address these concerns, the FORVES project introduces a verifier, leveraging formal verification techniques to ensure optimized bytecode retains its original semantics. By employing Coq, a rigorously verified proof assistant and programming language, FORVES enhances trust in optimization processes, shifting the burden of proof from the optimizer to the verifier. This project outlines the development of FORVES2, an advanced iteration, which incorporates contextual information to assess code equivalence. Specifically, the project aims to devise an implication checker capable of verifying whether certain octagonal constraints hold in specific contexts, by employing a tightened transitive closure algorithm for validation.La optimización del bytecode de la máquina virtual de Ethereum (EVM) presenta retos y oportunidades únicos debido a sus requisitos específicos, que incluyen consideraciones como el coste de ejecución y el tamaño del ejecutable compilado. A pesar de sus potenciales beneficios, la optimización en este ámbito sigue siendo limitada, principalmente debido a los altos riesgos asociados con los programas EVM, llamados contratos inteligentes, donde incluso errores menores pueden resultar en pérdidas financieras significativas. Para abordar estas preocupaciones, el proyecto FORVES desarrolla un verificador, aprovechando las técnicas de verificación formal para garantizar que el código de bytes optimizado conserve su semántica original. Al emplear Coq, un asistente de pruebas y lenguaje de programación rigurosamente verificado, FORVES aumenta la confianza en los procesos de optimización, trasladando la carga de la prueba del optimizador al verificador. Este trabajo ocurre en el entorno de FORVES2, un sucesor del proyecto anterior que incorpora información contextual para evaluar la equivalencia del código. En concreto, el proyecto pretende diseñar un verificador de implicaciones capaz de comprobar si ciertas restricciones octogonales se cumple en contextos específicos, empleando para su validación un algoritmo de cálculo del cierre transitivo.