Szimbolikus tesztelés Halmossal: A meglévő tesztek felhasználása a formális ellenőrzéshez

A formális ellenőrzés – a program vagy az intelligens szerződés tetszőleges számú bemeneten keresztüli „ellenőrzésére” történő matematikai módszerekkel történő alkalmazása – általában a hagyományos tesztelés tömörebb, átfogóbb alternatívája a jobb minőségű, biztonságosabb kód írására. A valóságban azonban a formális ellenőrzés nyílt végű és interaktív folyamat. Hasonlóan az egységteszthez, a fejlesztőknek dinamikusan kell meghatározniuk és rétegezniük kell a formális specifikációkat, megismételve megközelítésüket, ahogyan kódjuk és elemzéseik fejlődnek. Ezenkívül a formális ellenőrzés csak annyira hatékony, mint a specifikációi, amelyek írása időigényes lehet (és gyakran meredek tanulási görbével jár). 

Sok fejlesztő számára, akik ijesztőnek találják a folyamatot, gyakran az egységtesztek jelentik a költséghatékonyabb és időtakarékosabb utat a program helyességének megállapításához. A gyakorlatban a formális ellenőrzés nem az egységtesztelés átfogóbb alternatívája, hanem kiegészítője. Ezeknek az eljárásoknak különböző erősségei és korlátai vannak, így együtt alkalmazva még nagyobb biztonságot nyújtanak. A fejlesztőknek mindig egységteszteket kell írniuk – mi lenne, ha ugyanazokat a tulajdonságokat használhatnánk a formális ellenőrzéshez?

Halmos, nyílt forráskódú formális ellenőrző eszközünk, amely lehetővé teszi a fejlesztők számára újra ugyanazok a tulajdonságok, amelyeket a formális specifikációk egységtesztjéhez írnak le szimbolikus teszteléssel. Ahelyett, hogy kezdettől fogva robusztus tulajdonságkészletet kellene létrehozniuk, a fejlesztők elkerülhetik a párhuzamos munkavégzést, és néhány specifikációnként javíthatják teszteiket anélkül, hogy a nulláról kezdenék. Ezt az eszközt úgy terveztük, hogy a formális ellenőrzési folyamatban másokkal együtt használjuk a formális ellenőrzés felé vezető úton; a fejlesztők minimális erőfeszítéssel kezdhetnek néhány elemzéssel, mielőtt később továbbiakat adnának hozzá.

Ebben a bejegyzésben bemutatjuk a formális ellenőrzés kihívásait, és azt a lehetőséget, hogy szimbolikus teszteléssel áthidaljuk az egységteszt és a formális ellenőrzés közötti szakadékot. Ezután végigsétálunk a Halmos bemutatóján a meglévő intelligens szerződéskóddal, és gyorsan áttekintjük a fejlesztők számára elérhető egyéb hivatalos ellenőrző eszközöket (sok nyílt forráskódú).

Formális ellenőrzés kontra tesztelés

Hivatalos ellenőrzés – amelyet a blokklánc-fejlesztők általában kedvelnek szigorúsága és átfogósága miatt – a program helyességének bizonyításának folyamata annak ellenőrzésével, hogy megfelel-e bizonyos helyességi tulajdonságoknak. A programra jellemző tulajdonságokat általában kívülről biztosítják, és olyan formális nyelven vagy jelöléssel fejezik ki, amelyet a használt ellenőrző eszköz támogat. A fejlesztők a formális ellenőrzést gyakran egy nyomógombos megoldásnak tekintik a tulajdonságok minden lehetséges forgatókönyv szerinti automatikus tesztelésére, de a valóságban a formális ellenőrzés munkaigényes és rendkívül interaktív folyamat lehet.

A formális ellenőrzéshez hasonlóan az egységteszt is magában foglalja annak értékelését, hogy egy program az elvárásoknak megfelelően működik-e; A tesztelés azonban csak a program viselkedését ellenőrzi néhány bemeneteket, míg a formális ellenőrzés ellenőrizheti minden lehetséges bemenetek. Mind a teszteléshez, mind a formális ellenőrzéshez szükség van a program várható viselkedésének leírására (a teszteléshez használt tesztesetekkel és a formális ellenőrzés során használt formális specifikációkkal). Együtt használva azonban alaposabb vizsgálatot tudnak biztosítani a programról. A tesztelés például hatékony az egyszerű hibák és hibák megtalálásában, de általában gyorsabban és könnyebben végrehajtható. A formális ellenőrzés, bár bonyolultabb a használata, elég hatékony ahhoz, hogy igazolja a hibák hiányát, vagy olyan finom hibákat tárjon fel, amelyeket könnyű kihagyni a tesztelés vagy a kódellenőrzés során.

Specifikáció rezsi

A formális ellenőrzés egyik fő kihívása a formai előírások írásának és karbantartásának többletköltsége. Ez a folyamat gyakran időigényes feladattal jár, amikor a specifikációkat speciális nyelven kézzel kell megírni (ezt sok fejlesztőnek először meg kell tanulnia). A folyamat szintén növekményes, jellemzően az egyszerű tulajdonságok írásával kezdődik, és először ellenőrzi azokat, majd fokozatosan ad hozzá összetettebb tulajdonságokat a tetejére. A teszteléshez hasonlóan ez is egy nyílt végű folyamat, nincs egyértelmű megállási pontja, és a rendelkezésre álló időkereten belül csak a lehető legtöbb tulajdonságot lehet hozzáadni. Ezenkívül, amikor a fejlesztők módosítják a kódot az ellenőrzés alatt, frissíteniük kell meglévő specifikációikat is, ami további karbantartási erőfeszítéseket tesz lehetővé. Ezek a tényezők ijesztő feladattá tehetik a formális ellenőrzést egyes fejlesztők számára, akik haboznak elköteleződni a többletköltség mellett.

És bár a tesztelés és a formális ellenőrzés javíthatja a kód minőségét, ha együtt használják, mindkettő (néha hasonló) leírást igényel a program várható viselkedéséről különböző nyelveken és formátumokban. E leírások megírása és karbantartása munkaigényes, és ugyanazon leírás két különböző formájának fenntartása megkettőzött erőfeszítésnek tűnhet. Ez felveti a következő kérdést: Lehetséges-e az elvárt viselkedést úgy leírni, hogy a fejlesztők mind tesztelésre, mind ellenőrzésre felhasználhassák?

A tesztelés és a formális ellenőrzés közötti szakadék áthidalása szimbolikus teszteléssel és Halmossal

A szimbolikus tesztelés, a szimbolikus bemenetekkel végzett tesztek gyakorlata, hatékony formális ellenőrzési módszer, amely csökkenti a specifikáció többletköltségét. Ez a megközelítés lehetővé teszi ugyanazon tesztesetek használatát mind a teszteléshez, mind a formális ellenőrzéshez. Ellentétben a hagyományos teszteléssel, amely ellenőrzi, hogy egy program megfelelően működik-e korlátozott számú bemenet esetén, a szimbolikus tesztelés minden lehetséges bemenetre ellenőrzi a programot, ezért a szimbolikus tesztelést áteső program formálisan ellenőrzöttnek tekinthető.

A Halmos egy formális ellenőrző eszköz, amelyet szimbolikus tesztelésre terveztek. A Halmos külön specifikációk megkövetelése vagy új nyelv tanulása helyett a meglévő teszteket használja formális specifikációként. A Halmoson keresztüli tesztek futtatása automatikusan ellenőrzi, hogy megfelelnek-e az összes lehetséges bemenetre, vagy ellenpéldákat szolgáltat. Ez nemcsak szükségtelenné teszi a további specifikációk írását, hanem lehetővé teszi az egységtesztelés vagy összemosás céljából írt tesztek újrafelhasználását formális ellenőrzési célokra.

A fejlesztők így nagyobb rugalmassággal választhatnak a minőségbiztosítási lehetőségek közül, beleértve az egységtesztet, a fuzzingot és a formális ellenőrzést, aktuális igényeiktől függően. Például a tesztek gyorsan azonosíthatják az egyszerű hibákat, esetleg egy véletlenszerű bemeneteket generáló fuzzer segítségével, majd a Halmos tovább növelheti a program helyességébe vetett bizalmat az összes bemeneten.

Példa: Tesztelve a isPowerOfTwo() funkció

Példaként vegye figyelembe a következőket isPowerOfTwo() függvény, amely meghatározza, hogy egy adott szám kettő hatványa-e. Ez a funkció a bit manipulációs algoritmus a hatékonyság érdekében, de kihívást jelenthet a helyességének bizonyítása, különösen abban az esetben, ha a bemenet nem kettős hatvány.

Képzelje el a következő tesztet a isPowerOfTwo() függvény: összehasonlítja a függvény tényleges kimenetét az adott bemenet várható kimenetével. Ez egy paraméterezett teszt (más néven tulajdonság-alapú teszt), ami azt jelenti, hogy könnyen futtatható különböző bemeneti értékekkel, esetleg olyan zavaró eszközökkel, mint a Foundry.

Ezzel a teszttel megvizsgálhatja a isPowerOfTwo() egységteszten vagy fuzzteszten keresztül működhet, és kiválasztott bemenetekkel futtathatja. Az ilyen tesztek formálisan nem tudják bizonyítani a függvény helyességét, mivel számításilag lehetetlen minden lehetséges bemenetre lefuttatni a tesztet.

A Halmos azonban lehetővé teszi a fejlesztők számára, hogy csak kis erőfeszítéssel újra felhasználják ezeket a már meglévő teszteket formális ellenőrzéshez. Az eszköz ellenőrzi, hogy a tesztek megfelelnek-e az összes lehetséges bemenetre úgy, hogy szimbolikusan végrehajtja a tesztet, majd ellenőrzi, hogy az állítást soha nem sértették-e meg (vagy ha az állítást is sérülnek, ellenpélda megadásával). Ez azt jelenti, hogy ha a teszt megfelel Halmoson, akkor a függvény helyessége formálisan igazolódik, vagyis az algoritmus megfelelően van implementálva, és a fordító pontosan lefordította bájtkódra.

Korlátozás: Korlátozott szimbolikus végrehajtás

Teljesen automatikus, teljes szimbolikus tesztelés általában nem végezhető el, mivel ehhez meg kellene oldani a leállási probléma, ami köztudottan az eldönthetetlen. Ennek egyik oka, hogy gyakran lehetetlen automatikusan meghatározni, hogy egy ciklusnak hányszor kell szimbolikusan megismétlődnie. Ennek eredményeként a teljesen automatikus formális ellenőrzés általában eldönthetetlen.

Tekintettel ezekre az alapvető korlátokra, a Halmos az automatizálást helyezi előtérbe a teljességgel szemben. Ennek érdekében a Halmost úgy tervezték, hogy korlátos szimbolikus érvelést hajtson végre korlátlan hurkok (ahol az iterációk száma a program bemeneteitől függ) vagy változó hosszúságú tömbök (beleértve a karakterláncokat is). Ez feláldoz némi teljességgel, de lehetővé teszi a Halmos számára, hogy elkerülje, hogy a felhasználónak további megjegyzéseket, például hurokinvariánsokat kelljen megadnia.

Vegyük például a következő iteratív változatát isPowerOfTwo() függvény, amely egy határtalan while ciklust tartalmaz, ahol a hurok iterációinak számát a bemeneti szám megjelenítéséhez szükséges bitek minimális száma határozza meg.

Halmos szimbolikusan csak egy meghatározott korlátig iterálja ezt a korlátlan hurkot. Például, ha a korlát 3-ra van állítva, Halmos legfeljebb 3-szor iterálja a ciklust, és nem veszi figyelembe azokat a bemeneti értékeket, amelyek miatt a hurok 3-nál többször ismétlődik (azaz minden 2^3-nál nagyobb vagy azzal egyenlő érték ). Ebben a konkrét esetben a korlát 256-ra vagy magasabbra állítása lehetővé tenné, hogy a Halmos teljes legyen.

Demo: ERC721A hivatalos ellenőrzése Halmossal

A Halmos képességeinek bemutatására szimbolikusan teszteltük és formálisan ellenőriztük ERC721A, az ERC721 szabvány nagymértékben gázoptimalizált megvalósítása, amely lehetővé teszi a kötegelt pénzverést szinte ugyanolyan költséggel, mint az egyszeri pénzverés. Az ERC721A számos innovatív elemet tartalmaz optimalizáció e hatékonyság elérése érdekében; Például gázt takaríthatunk meg, ha a token tulajdoni adatainak frissítését a token átviteléig késleltetjük, nem pedig a pénzverés időpontjában. Ez összetett adatstruktúrák és algoritmusok használatát teszi szükségessé a tulajdonosi információk hatékony lekéréséhez a lusta adatstruktúrából. És bár ez az optimalizálás javítja a gázhatékonyságot, a kód bonyolultságát is növeli, és kihívást jelent az implementáció helyességének bizonyítása. Ezáltal az ERC721A jó jelölt a formális ellenőrzéshez, mivel növelheti a megvalósításba vetett bizalmat, és előnyös a potenciális felhasználók számára.

Szimbolikus vizsgálati tulajdonságok

Mivel az ERC721A meglévő tesztjeit JavaScriptben írták Hardhat-tal (ezt jelenleg nem támogatja a Halmos), ezért új teszteket írtunk a Solidity-ben a fő belépési pont funkciókhoz: mint(), burn()és transfer(). Ezek a tesztek ellenőrizték, hogy minden egyes funkció megfelelően frissíti-e a token tulajdonjogát és egyenlegét, és csak az érintett felhasználókra van hatással anélkül, hogy megváltoztatná a többi felhasználó egyenlegét vagy tulajdonjogát. Ez utóbbit nem triviális bizonyítani az ERC721A lusta adatszerkezeti algoritmusa miatt. Például a következő teszt ellenőrzi, hogy a transfer() függvény megfelelően frissíti a megadott token tulajdonjogát:

Egy másik teszt ellenőrzi, hogy a transfer() függvény nem változtatja meg a többi cím egyensúlyát, amit nehéz bizonyítani, mint korábban említettük:

Ellenőrzési eredmények

Ellenőrző kísérletet hajtottunk végre Halmos segítségével az ERC721A okosszerződésen összesen írással 19 XNUMX teszt. A tesztek Halmoson futottak le 3-as huroktekercselő korláttal, ami 16 percet vett igénybe. Az ellenőrzési idő lebontása az alábbi táblázatban látható. A kísérletet M1 Pro chippel és 16 GB memóriával ellátott MacBook Pro-n végezték.

Teszt	Idő (k)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
testBurnOtherBalancePreservation	5.69
testBurnOtherOtherOwnershipPreservation	189.70
testBurnOwnershipUpdate	3.81
testBurnRequirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintOtherOtherOwnershipPreservation	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testTransferBalanceUnchanged	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdUnchanged	4.47
testTransferOtherBalancePreservation	19.57
testTransferOtherOtherOwnershipPreservation	430.61
testTransferOwnershipUpdate	18.71
tesztTransferRequirements	149.18

Míg a tesztek többsége pillanatok alatt elkészült, néhányuk több percig is eltartott. Ezeket az időigényes teszteket nehéz volt ellenőrizni a figyelembe veendő esetek összetettsége miatt, és szorosan összefüggtek a lusta adatszerkezeti algoritmus helyességével.

Összességében a kísérlet eredményei azt mutatják, hogy a Halmos képes hatékonyan ellenőrizni az intelligens szerződéskód helyességét. Az intelligens szerződés összetettsége és esetleges szélsőséges esetei ellenére fokozott bizalmat biztosít a kód integritásában.

Kísérletezzen a befecskendezett hibákkal

A Halmos-féle korlátolt érvelés hatékonyságának demonstrálására felhasználtuk az ERC721A szerződés korábbi verziójában található hibák észlelésére. Ebben a verzióban volt egy olyan probléma, amely rosszul kezelte az aritmetikai túlcsordulást, és potenciálisan lehetővé tette nagyszámú token kötegelt verését, ami megtörhette a lusta adatstruktúra integritását, és egyes felhasználók elvesztését eredményezhette a token tulajdonjogától (probléma megoldódott a jelenlegi verzióban). Ugyanezt a 19 tesztből álló ERC721A-t futtattuk a bugos változaton is, és Halmos ellenpéldát tudott találni az ERCXNUMXA tulajdonságaira. mint() funkció. Pontosabban, Halmos olyan bemeneti értékeket adott meg, amelyek a fent leírt kihasználási forgatókönyvhöz vezettek. A kísérlet eredményei azt mutatják, hogy a Halmos-féle korlátos érvelés hiányossága ellenére hatékony módja lehet az intelligens szerződések kihasználható hibáinak észlelésének és megelőzésének.

Kapcsolódó munka

Az Ethereum intelligens szerződés bytecode formális ellenőrző eszközeit különböző csapatok fejlesztették ki. Ezekkel az eszközökkel, így a Halmossal is, az okosszerződések biztonságát és helyességét biztosíthatjuk. Ezen eszközök különböző funkcióinak, képességeinek és korlátainak összehasonlítása és megértése segíthet a fejlesztőknek kiválasztani az egyedi igényeiknek leginkább megfelelőt.

Míg a Halmos értékes kiegészítője az intelligens szerződés-ellenőrzéshez rendelkezésre álló eszközkészletnek, célja, hogy kiegészítse (nem helyettesítse) a meglévő eszközöket. A fejlesztők a Halmost más eszközökkel is kombinálhatják, hogy magasabb szintű biztonságot érjenek el szerződéseikben. Az alábbiakban összehasonlítjuk a Halmost néhány kiválasztott formális eszközzel, amelyek támogatják az EVM bájtkódot.

• K egy hatékony formális ellenőrző keretrendszer, amely lehetővé teszi a deduktív ellenőrzést és az interaktív tételbizonyítást. Alapvető elmélete és megvalósítása magas szintű kifejezőkészséget biztosít, így alkalmas összetett programok és algoritmusok ellenőrzésére. Meg kell azonban jegyezni, hogy a K-t nem nagy hangsúlyt helyezve az automatizált ellenőrzésre, és hiányoznak bizonyos automatizálási funkciók, amelyek több kézi erőfeszítést igényelhetnek az ellenőrzési folyamat során. A K keretrendszer használatához a formális specifikációk K nyelven vannak megírva, amelyeket használat előtt meg kell tanulni. Erőssége különösen hasznos összetett rendszerek ellenőrzésében, amelyek automatizált érveléssel történő elemzése kihívást jelenthet.
• Certora egy formális ellenőrző eszköz az intelligens szerződésekhez, amely az automatizált ellenőrzésre összpontosít, és a Halmoshoz hasonlóan támogatja a korlátos modellellenőrzést. A Certora használatához a fejlesztőknek meg kell tanulniuk az új nyelvet, CVL, specifikációk írásához. Ez a nyelv lehetővé teszi számos kritikus tulajdonság tömör leírását a szerződésinvariánsokon keresztül, amit a Halmos jelenleg nem támogat. Annak ellenére, hogy zárt forráskódú, szabadalmaztatott eszköz, a Certora robusztus formális ellenőrzési eszközöket biztosít, folyamatos fejlesztéssel és jó felhasználói támogatással.
  
  Ezzel szemben a Halmos egy nyílt forráskódú eszköz, amely kisebb léptékű, és jelenleg hiányzik néhány Certora szolgáltatás, de közjót hivatott szolgálni, és résmegoldásként szolgál az intelligens szerződések gyors ellenőrzéséhez anélkül kiterjedt beállítás és karbantartás szükségessége.
• HEVM egy másik formális ellenőrző eszköz, amely hasonló a Halmoshoz. Korábban a DappTools része volt, amely a Foundry előfutára. Mind a HEVM, mind a Halmos rendelkezik azzal a tulajdonsággal, hogy nem igényel külön specifikációt, és szimbolikusan képes végrehajtani a meglévő teszteket az állítások megsértésének azonosítására. Ez lehetővé teszi a felhasználók számára, hogy mindkét eszközt felváltva, vagy párhuzamosan futtassák ugyanazokhoz a tesztekhez, több lehetőséget biztosítva számukra a szimbolikus teszteléshez.
  
  Érdemes megjegyezni, hogy hasonlóságaik ellenére a HEVM és a Halmos egymástól függetlenül fejlesztették ki, és megvalósítási részleteiben különböznek egymástól; különösen az optimalizálás és a szimbolikus érvelési stratégiák tekintetében. Ezenkívül a HEVM Haskell, míg a Halmos Python nyelven íródott, így a gazdag Python ökoszisztéma látható. Mindkét eszköz használatának lehetősége nagyobb rugalmasságot és lehetőséget biztosít a felhasználóknak az intelligens szerződések biztonságának és helyességének biztosítására.

Halmos nyílt forráskódú, és jelenleg a béta fázisban van. Aktívan dolgozunk az újdonságokon jellemzők és funkcionalitás, beleértve a Foundry csalási kódokat és számos más kulcsfontosságú használhatósági funkciót. Nagyra értékelnénk a legfontosabb funkciókkal kapcsolatos gondolatait, és szívesen fogadunk minden visszajelzést, javaslatot és hozzájárulást annak érdekében, hogy a Halmos mindenki számára jobb eszköz legyen.

**

Az itt kifejtett nézetek az AH Capital Management, LLC („a16z”) egyes alkalmazottainak nézetei, és nem az a16z vagy leányvállalatai nézetei. Az itt található bizonyos információk harmadik féltől származnak, többek között az a16z által kezelt alapok portfólióvállalataitól. Noha megbízhatónak vélt forrásokból származnak, az a16z nem ellenőrizte önállóan ezeket az információkat, és nem tesz kijelentést az információk aktuális vagy tartós pontosságáról, illetve annak egy adott helyzetre való megfelelőségéről. Ezenkívül ez a tartalom harmadik féltől származó hirdetéseket is tartalmazhat; az a16z nem vizsgálta át az ilyen hirdetéseket, és nem támogatja az abban található reklámtartalmat.

Ez a tartalom csak tájékoztatási célokat szolgál, és nem támaszkodhat rá jogi, üzleti, befektetési vagy adótanácsadásként. Ezekkel a kérdésekkel kapcsolatban konzultáljon saját tanácsadójával. Bármely értékpapírra vagy digitális eszközre történő hivatkozások csak illusztrációs célt szolgálnak, és nem minősülnek befektetési ajánlásnak vagy ajánlatnak befektetési tanácsadási szolgáltatások nyújtására. Ezen túlmenően ez a tartalom nem befektetőknek vagy leendő befektetőknek szól, és nem is szánható felhasználásra, és semmilyen körülmények között nem támaszkodhat rá az a16z által kezelt alapokba történő befektetésről szóló döntés meghozatalakor. (A16z alapba történő befektetésre vonatkozó ajánlatot csak az ilyen alap zártkörű kibocsátási memoranduma, jegyzési szerződése és egyéb vonatkozó dokumentációja tesz, és azokat teljes egészében el kell olvasni.) Minden említett, hivatkozott befektetés vagy portfóliótársaság, ill. A leírtak nem reprezentatívak az a16z által kezelt járművekbe történő összes befektetésre, és nem garantálható, hogy a befektetések nyereségesek lesznek, vagy a jövőben végrehajtott egyéb beruházások hasonló tulajdonságokkal vagy eredménnyel járnak. Az Andreessen Horowitz által kezelt alapok befektetéseinek listája (kivéve azokat a befektetéseket, amelyek esetében a kibocsátó nem adott engedélyt az a16z számára a nyilvánosságra hozatalra, valamint a nyilvánosan forgalmazott digitális eszközökbe történő be nem jelentett befektetéseket) a https://a16z.com/investments oldalon érhető el. /.

A benne található diagramok és grafikonok kizárólag tájékoztató jellegűek, és nem szabad rájuk hagyatkozni befektetési döntések meghozatalakor. A múltbeli teljesítmény nem jelzi a jövőbeli eredményeket. A tartalom csak a feltüntetett dátum szerint beszél. Az ezekben az anyagokban megfogalmazott előrejelzések, becslések, előrejelzések, célok, kilátások és/vagy vélemények előzetes értesítés nélkül változhatnak, és mások véleményétől eltérhetnek vagy ellentétesek lehetnek. További fontos információkért látogasson el a https://a16z.com/disclosures oldalra.