Verification of Solidity: Data Types, Memory Models, and Inheritance
| dc.contributor.author | Ekgrim , Christoffer | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data och informationsteknik | sv |
| dc.contributor.department | Chalmers University of Technology / Department of Computer Science and Engineering | en |
| dc.contributor.examiner | Angelov, Krasimir | |
| dc.contributor.supervisor | Ahrendt, Wolfgang | |
| dc.date.accessioned | 2022-11-23T10:22:28Z | |
| dc.date.available | 2022-11-23T10:22:28Z | |
| dc.date.issued | 2022 | |
| dc.date.submitted | 2020 | |
| dc.description.abstract | Smart contracts are programs on the Ethereum blockchain that can not only hold, send, and receive ether – the native cryptocurrency of Ethereum – but can also record and reinforce transactions made with it. A contract consists of data and functions, and user accounts may interact with the contract by invoking one of these functions, resulting in a protocol enforced by the contract’s internal logic. Often, smart contracts are written in Solidity – a programming language inspired by C++ and Python. The functional correctness of these contracts is crucial; potential bugs could be exploited, which could result in the contract’s users incurring major financial losses. Thus, tools exist for formally verifying contracts written in Solidity. SolidiKeY is one such prototype tool, being based on the tool KeY. It uses deductive verification and works by interpreting the statements of a function one-by-one and using calculus rules to draw conclusions about its behavior. However, SolidiKeY does not yet cover or model all aspects of the Solidity language. In this thesis project, we aimed to extend SolidiKeY’s coverage of Solidity. We were able to improve SolidiKeY’s support for contract inheritance, function modifiers, and libraries, among other things, by making SolidiKeY transform input contracts so that they are more compatible with the KeY aspect of SolidiKeY. Moreover, we implemented a model of storage, which now allows SolidiKeY to reason correctly about the copy semantics for assignments made within storage. However, this modeling remains incomplete, e.g., SolidiKeY does not yet model local storage variables. Furthermore, SolidiKeY’s support for mappings is still poor. Once these difficulties have been sorted out, SolidiKeY is set to become an excellent tool for smart contract verification. | |
| dc.identifier.coursecode | DATX05 | |
| dc.identifier.uri | https://odr.chalmers.se/handle/20.500.12380/305822 | |
| dc.language.iso | eng | |
| dc.setspec.uppsok | Technology | |
| dc.subject | deductive verification | |
| dc.subject | Ethereum | |
| dc.subject | formal verification | |
| dc.subject | KeY | |
| dc.subject | smart contracts | |
| dc.subject | SolidiKeY | |
| dc.subject | Solidity | |
| dc.title | Verification of Solidity: Data Types, Memory Models, and Inheritance | |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.degree | Master's Thesis | en |
| dc.type.uppsok | H | |
| local.programme | Computer science – algorithms, languages and logic (MPALG), MSc |