Formal Verification of Smart Contracts on the Ethereum Platform

Student: Skvortsov Grigory

Supervisor: Rostislav Yavorskiy

Educational Programme: Applied Mathematics and Information Science (Bachelor)

Year of Graduation: 2018

Blockchain is called the most breakthrough area at the turn of computer, financial and legal sciences of the XXI century. The technology has many applications, including smart contracts. The most popular platform for the design and execution of smart contracts is Ethereum. Smart contracts can be used for a variety of purposes, for example, in systems for organizing elections, division of inheritance, real estate rental and stock trading. In other words, they are used for the exchange and transfer of assets, the value of which can reach huge values. For this reason, the consequences of a mistake in a smart contract can be critical. For this reason, the problem of writing a safe and effective contract is laborious and important. Due to some features of the blockchain systems architecture, the use of classical testing is not suitable for debugging the behavior of smart contracts. In this diploma project, we will talk about one of the approaches to prove the correctness of programs - formal verification, consider the mechanism of the blockchain technology in feneral and the Ethereum project, and also consider the possibility of applying formal verification to smart contracts on this platform. Keywords: Formal verification, smart contract, Blockchain, Ethereum, cryptocurrency, Isabelle, theorem prover, model checking.

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses