UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Synthesis of Super-Optimized Smart Contracts Using Max-SMT

Albert, E; Gordillo, P; Rubio, A; Schett, MA; (2020) Synthesis of Super-Optimized Smart Contracts Using Max-SMT. In: Computer Aided Verification. (pp. pp. 177-200). Springer: Cham, Switzerland. Green open access

[thumbnail of Albert2020_Chapter_SynthesisOfSuper-OptimizedSmar.pdf]
Albert2020_Chapter_SynthesisOfSuper-OptimizedSmar.pdf - Published Version

Download (1MB) | Preview


With the advent of smart contracts that execute on the blockchain ecosystem, a new mode of reasoning is required for developers that must pay meticulous attention to the gas spent by their smart contracts, as well as for optimization tools that must be capable of effectively reducing the gas required by the smart contracts. Super-optimization is a technique which attempts to find the best translation of a block of code by trying all possible sequences of instructions that produce the same result. This paper presents a novel approach for super-optimization of smart contracts based on Max-SMT which is split into two main phases: (i) the extraction of a stack functional specification from the basic blocks of the smart contract, which is simplified using rules that capture the semantics of the arithmetic, bit-wise, relational operations, etc. (ii) the synthesis of optimized blocks which, by means of an efficient Max-SMT encoding, finds the bytecode blocks with minimal gas cost whose stack functional specification is equal (modulo commutativity) to the extracted one. Our experimental results are very promising: we are able to optimize 55.41 % of the blocks, and prove that 34.28 % were already optimal, for more than 61000 blocks from the most called 2500 Ethereum contracts.

Type: Proceedings paper
Title: Synthesis of Super-Optimized Smart Contracts Using Max-SMT
Event: CAV 2020
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-030-53288-8_10
Publisher version: https://doi.org/10.1007/978-3-030-53288-8_10
Language: English
Additional information: This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10113344
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item