dc.contributor.author | Marmsoler, D | |
dc.contributor.author | Brucker, AD | |
dc.date.accessioned | 2021-10-18T10:19:53Z | |
dc.date.issued | 2021-12-03 | |
dc.description.abstract | Smart contracts are programs, usually automating legal agreements such as financial transactions. Thus, bugs in smart contracts can lead to large financial losses. For example, an incorrectly initialized contract was the root cause of the Parity Wallet bug that made USD 280mil worth of Ether inaccessible. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing smart contracts. In this paper, we address this problem by presenting an executable denotational semantics for Solidity in the interactive theorem prover Isabelle/HOL. This formal semantics builds the foundation of an interactive program verification environment for Solidity programs and allows for inspecting Solidity programs by (symbolic) execution. We combine the latter with grammar-based fuzzing to ensure that our formal semantics complies to the Solidity implementation on the Ethereum Blockchain. Finally, we demonstrate the formal verification of Solidity programs by two examples: constant folding and memory optimization. | en_GB |
dc.identifier.citation | Vol. 13085, pp. 403 - 422 | en_GB |
dc.identifier.doi | 10.1007/978-3-030-92124-8_23 | |
dc.identifier.uri | http://hdl.handle.net/10871/127493 | |
dc.language.iso | en | en_GB |
dc.publisher | Springer Verlag | en_GB |
dc.rights | © Springer Nature Switzerland AG 2021 | |
dc.subject | Solidity | en_GB |
dc.subject | Denotational Semantics | en_GB |
dc.subject | Isabelle/HOL | en_GB |
dc.subject | Gas Optimization. | en_GB |
dc.title | A Denotational Semantics of Solidity in Isabelle/HOL | en_GB |
dc.type | Conference paper | en_GB |
dc.date.available | 2021-10-18T10:19:53Z | |
dc.contributor.editor | Calinescu, R | en_GB |
dc.contributor.editor | Pasareanu, C | en_GB |
dc.identifier.issn | 0302-9743 | |
exeter.place-of-publication | Heidelberg | en_GB |
dc.description | This is the author accepted manuscript. The final version is available from Springer via the DOI in this record | en_GB |
dc.description | Availability. Our formalisation, the test framework, and the evaluation results
are available under BSD license (SPDX-License-Identifier: BSD-2-Clause) [24]. | en_GB |
dc.description | SEFM 2021: 19th International Conference on Software Engineering and Formal Methods, 6-10 December 2021 | en_GB |
dc.identifier.journal | Lecture Notes in Computer Science | en_GB |
dc.rights.uri | http://www.rioxx.net/licenses/all-rights-reserved | en_GB |
dcterms.dateAccepted | 2021 | |
rioxxterms.version | AM | en_GB |
rioxxterms.licenseref.startdate | 2021-10-18 | |
rioxxterms.type | Conference Paper/Proceeding/Abstract | en_GB |
refterms.dateFCD | 2021-10-18T10:18:25Z | |
refterms.versionFCD | AM | |
refterms.dateFOA | 2022-01-07T12:17:01Z | |
refterms.panel | B | en_GB |