RT Journal Article
T1 Super-optimization of Smart Contracts
A1 Albert Albiol, Elvira María
A1 Gordillo Alguacil, Pablo
A1 Hernández-Cerezo, Alejandro
A1 Rubio, Albert
A1 Schett, Maria A.
AB Smart contracts are programs deployed on a blockchain. They are executed for a monetary fee paid in gas—a clear optimization target for smart contract compilers. Because smart contracts are a young, fast-moving field without (manually) fine-tuned compilers, they highly benefit from automated and adaptable approaches, especially as smart contracts are effectively immutable, and as such need a high level of assurance. This makes them an ideal domain for applying formal methods. Super-optimization is a technique to find the best translation of a block of instructions by trying all possible sequences of instructions that produce the same result. We present a framework for super-optimizing smart contracts based on Max-SMT with two main ingredients: (1) a stack functional specification extracted from the basic blocks of a smart contract, which is simplified using rules capturing the semantics of arithmetic, bit-wise, and relational operations, and (2) the synthesis of optimized blocks, which finds—by means of an efficient SMT encoding—basic blocks with minimal gas cost whose stack functional specification is equal (modulo commutativity) to the extracted one. We implemented our framework in the tool syrup 2.0. Through large-scale experiments on real-world smart contracts, we analyze performance improvements for different SMT encodings, as well as tradeoffs between quality of optimizations and required optimization time.
PB Association for Computing Machinery
SN 1049-331X
YR 2022
FD 2022
LK https://hdl.handle.net/20.500.14352/96462
UL https://hdl.handle.net/20.500.14352/96462
LA eng
NO Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio, and Maria A. Schett. 2022. Super-optimization of Smart Contracts. ACM Trans. Softw. Eng. Methodol. 31, 4, Article 70 (October 2022), 29 pages. https://doi.org/10.1145/3506800
DS Docta Complutense
RD 10 abr 2025