Input Output demonstrira Blaster za verifikaciju pametnih ugovora na Cardanu

Cardano Community je objavila prezentaciju alata Blaster, automatiziranog alata za verifikaciju osmišljenog da provjeri prate li Cardano pametni ugovori zadana pravila. Inženjeri iz Input Outputa Romain Soulat i Jean-Frédéric Etienne pokazuju kako alat ispituje ta svojstva i može proizvesti protuprimjer kada pronađe kršenje. Raspravljaju i o tekućem radu na rekonstrukciji dokaza te načinima kako rezultate učiniti lakšima za pregled.

Definiranje onoga što Cardano ugovor mora činiti

Pametni ugovori postavljaju uvjete za transakcije na blockchainu i određuju kako aplikacije upravljaju imovinom. Programer može, na primjer, navesti da samo ovlašteni korisnik može otključati sredstva koja drži ugovor. Formalna verifikacija koristi matematičke metode kako bi provjerila zadovoljava li sustav svojstva zapisana u specifikaciji. Dok konvencionalni test ispituje odabrane slučajeve, formalna verifikacija nastoji utvrditi vrijedi li zadano svojstvo u svim slučajevima obuhvaćenima modelom.

Soulat, tehnički voditelj za Cardano High Assurance, objasnio je da je Blaster namijenjen automatiziranju većeg dijela dokaznog posla. Programeri i dalje trebaju definirati ponašanje koje žele provjeriti i priložiti odgovarajuću specifikaciju. Kada alat pronađe kršenje, može proizvesti protuprimjer za pregled. Soulat je opisao transakciju ili niz transakcija koji bi mogli pokazati kako netko tko nije ovlašteni korisnik otključava izlaz.

Kako Blaster provjerava svojstva ugovora

Blaster koristi Lean 4, sustav za izražavanje matematičkih iskaza i rad s dokazima, zajedno s automatiziranim rješavačem. Najprije pojednostavljuje problem; ako se svojstvo ne razriješi u toj fazi, preostali se problem može poslati rješavaču. Kako bi provjere bile relevantne za Cardano, tim je formalizirao dijelove okruženja u kojem ugovori rade, uključujući izvršavanje skripti i pravila transakcija.

Etienne, viši inženjer za formalne metode, iznio je tri moguća ishoda: svojstvo se može prijaviti kao valjano, opovrgnuto ili neodređeno. Protuprimjer povezan s opovrgnutim ishodom može pomoći programerima da prepoznaju grešku u ugovoru, propuštenu pretpostavku ili pogrešku u specifikaciji. Neodređeni ishod znači da rješavač nije utvrdio drži li svojstvo. Opseg provjere ovisi o svojstvima koja programeri odluče izraziti.

[NEWSBREAK]

Rekonstrukcija dokaza je u razvoju

Programeri mogu kompilirati ugovore napisane u jezicima kao što su Plinth, Aiken ili Plutarch u Untyped Plutus Core, reprezentaciju koja se koristi za izvršavanje Cardano skripti. Zatim mogu uvesti kompilirani kod u Lean 4 i zadati svojstva koja treba provjeriti. Input Output je ranije objavio dvije biblioteke otvorenog koda koje za ovaj proces pružaju modele specifične za Cardano. U ranijoj demonstraciji tim je primijenio taj radni tok na probni ugovor iz sigurnosnog izazova, generirajući kontekst transakcije koji je pokazao kako se ugovor može iskoristiti.

Etienne je objasnio da je rekonstrukcija dokaza još u razvoju. Cilj je omogućiti da Lean neovisno provjeri dokaze koji podupiru valjan ishod; trenutačni alat još ne proizvodi rekonstruiran Leanov dokaz kada rješavač vrati taj ishod. Soulat je također iznio planove za jasniji prikaz protuprimjera, kako bi programeri mogli pregledati detalje transakcije koji stoje iza neuspjelog svojstva.