Super-optimization of Smart Contracts

【Author】 Albert, Elvira; Gordillo, Pablo; Hernandez-Cerezo, Alejandro; Rubio, Albert; Schett, Maria A.

【Source】ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY

【影响因子】3.685

【Abstract】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.

【Keywords】Smart contracts; synthesis; optimization; Max-SMT solvers

【发表时间】2022 OCT

【收录时间】2022-10-05

【文献类型】理论模型

【主题类别】

区块链技术-核心技术-智能合约