Cargando…
SMT-Friendly Formalization of the Solidity Memory Model
Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the...
Autores principales: | , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7702262/ http://dx.doi.org/10.1007/978-3-030-44914-8_9 |
_version_ | 1783616579352657920 |
---|---|
author | Hajdu, Ákos Jovanović, Dejan |
author_facet | Hajdu, Ákos Jovanović, Dejan |
author_sort | Hajdu, Ákos |
collection | PubMed |
description | Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the SOLC-VERIFY verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools. |
format | Online Article Text |
id | pubmed-7702262 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-77022622020-12-01 SMT-Friendly Formalization of the Solidity Memory Model Hajdu, Ákos Jovanović, Dejan Programming Languages and Systems Article Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the SOLC-VERIFY verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools. 2020-04-18 /pmc/articles/PMC7702262/ http://dx.doi.org/10.1007/978-3-030-44914-8_9 Text en © The Author(s) 2020 Open Access 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. |
spellingShingle | Article Hajdu, Ákos Jovanović, Dejan SMT-Friendly Formalization of the Solidity Memory Model |
title | SMT-Friendly Formalization of the Solidity Memory Model |
title_full | SMT-Friendly Formalization of the Solidity Memory Model |
title_fullStr | SMT-Friendly Formalization of the Solidity Memory Model |
title_full_unstemmed | SMT-Friendly Formalization of the Solidity Memory Model |
title_short | SMT-Friendly Formalization of the Solidity Memory Model |
title_sort | smt-friendly formalization of the solidity memory model |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7702262/ http://dx.doi.org/10.1007/978-3-030-44914-8_9 |
work_keys_str_mv | AT hajduakos smtfriendlyformalizationofthesoliditymemorymodel AT jovanovicdejan smtfriendlyformalizationofthesoliditymemorymodel |