Verification of Solidity: Data Types, Memory Models, and Inheritance

Typ
Examensarbete för masterexamen
Master's Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2022
Författare
Ekgrim , Christoffer
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
deductive verification, Ethereum, formal verification, KeY, smart contracts, SolidiKeY, Solidity
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material