Formalno modeliranje procesa nadogradnje konsenzusa u kriptografskom lancu blokova

diplomski rad

• Naslov (engleski): Formally modelling soft-forks in blockchains
• Autor: Kristijan Rupić
• Mentor: Ante Đerek (mentor)
• Član povjerenstva: Ante Đerek (član povjerenstva)
• Član povjerenstva: Marin Golub (član povjerenstva)
• Član povjerenstva: Leonardo Jelenković (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Fakultet elektrotehnike i računarstva; Zagreb
• Datum i država obrane: 2021-07-02, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: TEHNIČKE ZNANOSTI; Računarstvo

Sažetak

Kriptografski lanac blokova (engl. blockchain) je raspodijeljena baza podataka koja koristeći kriptografiju i protokole raspodijeljenog konsenzusa osigurava
integritet i neporecivost pohranjenih informacija. Nepažljive promjene pravila
konsenzusa u takvom sustavu mogu uzrokovati raspad mreže pa ih je kako bi se
to izbjeglo poželjno implementirati kao takozvano meko račvanje (engl. soft-fork).
U sklopu diplomskog rada je izrađen formalan model soft-forkova u kriptografskim lancima blokova u interaktivnom asistentu za dokazivanje Coq. Na temelju
definicija izrađen je jednostavan programski okvir za olakšan razvoj formalno verificiranih soft-forkova, te primijenjen na postojeći model sustava Bitcoin s ciljem
modeliranja i pokušaja dokaza ispravnosti soft-forka opisanog u BIP 34.

Sažetak (engleski)

Blockchains are distributed databases which, using cryptography and distributed consensus protocols ensure the integrity and indisputability of stored information. Careless changes of the consesus rules of such systems can cause the
network to break apart; in order to avoid that it is desirable to implement these
changes as soft-forks. In this thesis a formal model of blockchain soft-forks is
developed in the interactive proof assistant Coq. Based on these definitions a
simple framework is built with the purpose of enabling simplified development
of formally verified soft-forks, and applied to an existing model of the Bitcoin
system with the purpose of modelling and proving correct the soft-fork described
in BIP 34.

• Ključne riječi: kriptografski lanac blokova; soft-fork; Bitcoin; mehanizirani dokaz; pomoćnik za dokazivanje; Coq
• Ključne riječi (engleski): blockchain; soft-fork; Bitcoin; mechanized proof; proof assistant; Coq
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:168:626047
• Studijski program: Naziv: Računarstvo; Vrsta studija: sveučilišni; Stupanj studija: diplomski; Akademski / stručni naziv: magistar/magistra inženjer/inženjerka računarstva (mag.ing.comp.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Zatvoreni pristup
• Datum i vrijeme pohrane: 2023-01-13 13:44:31