Naročite se na naše novice.

Email naslov

Spoštujemo vašo zasebnost

DomovBlogNovice

Predstavljamo Scribble s strani ConsenSys Diligence

avtor ConsenSys 8. december 2020 Objavljeno 8. decembra 2020

Zagotavljanje, da so pametne pogodbe varne in brez napak, še nikoli ni bilo bolj kritično. Na žalost ostaja težka naloga. Čeprav obstajajo koristna orodja za samodejno testiranje in formalno preverjanje, je zagotavljanje pravilnosti pametnih pogodb še vedno dolgotrajna in zahtevna naloga. Da je stvar še hujša, ima vsako orodje pogosto strmo učno krivuljo in pogosto je negotovo, ali je sploh primerno za to službo.

Zato smo razvili Scribble: jezik za preverjanje in orodje za preverjanje med izvajanjem. Čeprav je bil sprva ustvarjen za samodejno preskušanje nepremičnin med revizijami, smo se odločili, da ta projekt delimo s skupnostjo!

Kaj je Scribble?

Ko govorimo o Scribble, govorimo o dveh stvareh.

Prvič, Scribble je jezik specifikacije za zapisovanje lastnosti.

Drugič, Scribble je orodje za preverjanje izvajalnega okolja, ki uporablja jezik specifikacije Scribble.

OPOMBA: Scribble sam ne opravi nobenega preverjanja. To naredi omogoči druga orodja za preizkušanje in preverjanje lastnosti.

Škrabanje je jezik

Scribble definira jezik, specifičen za domeno, za pisanje lastnosti o pametnih pogodbah. Jezik smo zgradili nad sintakso solidity, da ga je lažje učiti. Ta jezik specifikacije vam omogoča, da trdne pametne pogodbe označite z lastnostmi.

OPOMBA: Lastnost je logična izjava, za katero pričakujete, da bo resnična, npr. “Vsi avtomobili so rdeči”. Kot trdnost boste pogosto imeli lastnosti, kot so: “Samo lastnik lahko spremeni X”. Ali “Funkcija sendToken (), ne sme spremeniti eterskega ravnotežja te pogodbe”.

Za različne vrste lastnosti lahko uporabite več vrst pripisov. Na primer, invariante ali post-pogoji.

To je primer pripisa Scribble:

Posnetek zaslona 2020 12. 08. ob 12. 06. 15

Kot lahko vidite, imajo pripisi obliko vstavljenega komentarja nad definicijo funkcije. Dodali smo tako imenovano klavzulo if_succeeds, ki preverja, ali stanje velja po izvedbi funkcije. V tem primeru preverimo, ali rezultat funkcije vedno ni nič.

Preberite pisarniško dokumentacijo

Jezik Scribble smo utemeljili na preizkušenih konceptih, kot so post-pogoji, invariante in časovna logika. Preučujemo pa tudi, kako lahko predstavimo nove ideje, ki bodo bolje ustrezale specifičnim problemom pametnih pogodb.

Scribble je orodje

Scribble lahko sprejme pogodbo, označeno z lastnostmi, in jo sestavi v novo pogodbo. V tej novi pogodbi bo Scribble dodal kodo Solidity, ki sproži trditev, kadar je lastnost kršena. Temu postopku pravimo instrumentacija.

Dodajanje izvršljive kode, ki preverja lastnosti, se imenuje preverjanje izvajalnega okolja in olajša delo z obstoječimi orodji brez veliko prilagoditev. To velja, ker bo večina orodij že razlagala solidnostno kodo in bo lahko takoj iskala kršitve lastnine!

Ker lahko uporabite obstoječe tehnike samodejnega testiranja (na primer naš fuzzer Harvey), boste lahko začeli s preskušanjem po pisanju samo ene lastnosti. Menimo, da je to pomembna korist; Takoj imate koristi od samodejnega testiranja, namesto da bi morali vnaprej porabiti veliko časa, da pridobite kritično maso pripisov. Nekaj, kar je običajno potrebno pri tradicionalnih pristopih preverjanja.

Hitro lahko začnete s testiranjem in analizo pogodbe, kasneje pa se celo odločite, da si boste dodatno prizadevali za popolno preverjanje pametne pogodbe!

Cilji

Revizija

Scribble uporabljamo med revizijami za oblikovanje lastnosti. Z uporabo samodejnih analiznih tehnik, kot sta mešanje in simbolična izvedba, bomo samodejno preizkusili in ugotovili kršitve teh lastnosti.

Pišite nam, če želite izvedeti več o nejasnostih in preskusih na podlagi lastnosti med revizijami

Standardno

Scribble želi delati z različnimi orodji in tehnikami; ne želimo samo omogočiti testiranja na podlagi lastnosti, ampak tudi enostavno formalno preverjanje. Prednost uporabe enega samega jezika univerzalne specifikacije je v tem, da se potrudite samo enkrat zapisati lastnosti, vendar izkoristite prednosti uporabe več orodij.

Posvojitev

S Scribble upamo, da bomo spustili pregrado ali vstop za samodejno testiranje in formalno preverjanje. Prav tako želimo zmanjšati čas, potreben za razvoj pravilnih in varnih pametnih pogodb, kar bo imelo za posledico varnejši ekosistem.