Input Output predstavi Blaster za preverjanje pametnih pogodb na Cardanu

Skupnost Cardano je objavila predstavitev orodja Blaster, avtomatiziranega orodja za preverjanje, zasnovanega za preverjanje, ali pametne pogodbe na Cardanu sledijo določenim pravilom. Inženirja Input Output, Romain Soulat in Jean-Frédéric Etienne, pokažeta, kako orodje preučuje te lastnosti in lahko ob zaznani kršitvi ustvari protiprimer. Govorita tudi o potekajočem delu na rekonstrukciji dokazov ter o načinih, kako rezultate narediti lažje pregledne.

Opredelitev, kaj mora pogodba na Cardanu storiti

Pametne pogodbe določajo pogoje za transakcije v verigi blokov in določajo, kako aplikacije ravnajo s sredstvi. Razvijalec lahko na primer določi, da lahko sredstva, ki jih drži pogodba, odklene le pooblaščeni uporabnik. Formalno preverjanje uporablja matematične metode, da se preveri, ali sistem izpolnjuje lastnosti, zapisane v specifikaciji. Medtem ko običajen test preizkusi izbrane primere, si formalno preverjanje prizadeva ugotoviti, ali navedena lastnost velja v vseh primerih, ki jih zajema model.

Soulat, tehnični vodja za Cardano High Assurance, je pojasnil, da je Blaster namenjen avtomatizaciji velikega dela dokazovanja. Razvijalci morajo še vedno opredeliti vedenje, ki ga želijo preveriti, in zagotoviti ustrezno specifikacijo. Ko orodje najde kršitev, lahko ustvari protiprimer za pregled. Soulat je opisal transakcijo ali zaporedje transakcij, ki bi lahko pokazalo, da izhod odklene nekdo, ki ni pooblaščeni uporabnik.

Kako Blaster preverja lastnosti pogodb

Blaster uporablja Lean 4, sistem za izražanje matematičnih izjav in delo z dokazi, skupaj z avtomatiziranim reševalnikom. Najprej poenostavi problem, če lastnosti v tej fazi ni mogoče razrešiti, se lahko preostali problem pošlje reševalniku. Da bi bila preverjanja ustrezna za Cardano, je ekipa formalizirala dele okolja, v katerem tečejo pogodbe, vključno z izvajanjem skriptov in pravili transakcij.

Etienne, višji inženir za formalne metode, je orisal tri možne izide: lastnost je lahko označena kot veljavna, ovržena ali nedoločena. Protiprimer, povezan z ovrženim izidom, lahko razvijalcem pomaga prepoznati napako v pogodbi, manjkajočo predpostavko ali napako v specifikaciji. Nedoločeni izid pomeni, da reševalnik ni ugotovil, ali lastnost drži. Obseg preverjanja je odvisen od lastnosti, ki se jih razvijalci odločijo izraziti.

[NEWSBREAK]

Rekonstrukcija dokazov je v razvoju

Razvijalci lahko pogodbe, napisane v jezikih, kot so Plinth, Aiken ali Plutarch, prevedejo v Untyped Plutus Core, predstavitev, ki se uporablja za izvajanje skriptov na Cardanu. Nato lahko prevedeno kodo uvozijo v Lean 4 in določijo lastnosti, ki jih je treba preveriti. Input Output je prej objavil dve odprtokodni knjižnici, ki za ta postopek zagotavljata za Cardano specifične modele. V zgodnejši predstavitvi je ekipa uporabila cevovod na vadbeni pogodbi iz varnostnega izziva in ustvarila kontekst transakcije, ki je pokazal, kako je mogoče pogodbo izkoristiti.

Etienne je pojasnil, da je rekonstrukcija dokazov še v razvoju. Cilj je, da Lean samostojno preveri dokaze, ki podpirajo veljaven izid, trenutno orodje še ne proizvaja rekonstruiranega dokaza v Leanu, ko reševalnik vrne tak izid. Soulat je orisal tudi načrte za bolj pregledne poglede protiprimerov, ki bodo razvijalcem omogočili pregled podrobnosti transakcije v ozadju spodletele lastnosti.