Verification of Solidity: Data Types, Memory Models, and Inheritance
Ladda ner
Typ
Examensarbete för masterexamen
Master's Thesis
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