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.
Preview |
Text
Albert2020_Chapter_SynthesisOfSuper-OptimizedSmar.pdf - Published Version Download (1MB) | Preview |
Abstract
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 |
Archive Staff Only
 |
View Item |
