Symbolisk testning med Halmos: Utnyttja befintliga tester för formell verifiering

Formell verifiering - processen att använda matematiska metoder för att "inspektera" ett program eller smart kontrakt över valfritt antal ingångar - ses i allmänhet som det mer kortfattade, mer omfattande alternativet till traditionella tester för att skriva säkrare kod av högre kvalitet. Men i verkligheten är formell verifiering en öppen och interaktiv process. Ungefär som enhetstestning måste utvecklare dynamiskt definiera och lägga på formella specifikationer, iterera på deras tillvägagångssätt allteftersom deras kod och analyser utvecklas. Vidare är formell verifiering bara lika effektiv som dess specifikationer, vilket kan vara tidskrävande att skriva (och ofta kommer med en brant inlärningskurva). 

För många utvecklare som tycker att processen är skrämmande är enhetstester ofta den mer kostnadseffektiva och tidseffektiva vägen för att avgöra om ett program är korrekt. I praktiken är formell verifiering inte ett mer omfattande alternativ till enhetstestning, utan ett komplement. Dessa processer har olika styrkor och begränsningar, vilket ger ännu större säkerhet när de används tillsammans. Utvecklare kommer alltid att behöva skriva enhetstester - så tänk om vi kunde använda samma egenskaper för formell verifiering?

Halmos, vårt formella verifieringsverktyg med öppen källkod, tillåter utvecklare att återanvända samma egenskaper skrivna för enhetstester för formella specifikationer genom symbolisk testning. Istället för att behöva skapa en robust uppsättning egenskaper från början, kan utvecklare undvika dubbelarbete och förbättra sina tester några specifikationer åt gången utan att börja om från början. Vi designade det här verktyget för att användas, tillsammans med andra i den formella verifieringsprocessen, som en påkörning till formell verifiering; utvecklare kan börja med några analyser med minimal ansträngning, innan de lägger till fler senare i processen.

I det här inlägget täcker vi utmaningarna med formell verifiering och potentialen att överbrygga gapet mellan enhetstestning och formell verifiering med symbolisk testning. Vi går sedan igenom en demo av Halmos med befintlig smart kontraktskod och tar en snabb titt på andra formella verifieringsverktyg (många öppen källkod) som är tillgängliga för utvecklare.

Formell verifiering kontra testning

Formell verifiering - allmänt gynnat av blockchain-utvecklare för dess rigoritet och omfattandehet - är processen att bevisa ett programs korrekthet genom att verifiera att det uppfyller vissa korrekthetsegenskaper. Egenskaperna, som är specifika för programmet, tillhandahålls vanligtvis externt och uttrycks med ett formellt språk eller notation som stöds av det verifieringsverktyg som används. Utvecklare uppfattar ofta formell verifiering som en tryckknappslösning för att testa egenskaper i alla möjliga scenarier automatiskt, men i verkligheten kan formell verifiering vara en arbetskrävande och mycket interaktiv process.

Liksom formell verifiering innebär enhetstestning att utvärdera om ett program fungerar som förväntat; testning kontrollerar dock bara programmets beteende för några ingångar, medan formell verifiering kan kontrollera det alla möjliga ingångar. Både testning och formell verifiering kräver en beskrivning av programmets förväntade beteende (med testfall som används vid testning och formella specifikationer som används vid formell verifiering). Men när de används tillsammans kan de ge en mer grundlig granskning av ett program. Testning är till exempel effektivt för att hitta enkla buggar och misstag, men är i allmänhet snabbare och lättare att utföra. Formell verifiering, även om den är mer besvärlig att använda, är tillräckligt kraftfull för att bevisa frånvaron av fel eller avslöja subtila buggar som är lätta att missa i testning eller kodgranskning.

Specifikation overhead

En av de största utmaningarna med formell verifiering är omkostnader för att skriva och underhålla formella specifikationer. Denna process innebär ofta den tidskrävande uppgiften att manuellt skriva specifikationerna med hjälp av ett specialiserat språk (som många utvecklare måste lära sig först). Processen är också inkrementell, vanligtvis börjar med att skriva enkla egenskaper och verifiera dem först, och sedan gradvis lägga till mer komplexa egenskaper ovanpå. Liksom testning är det en öppen process, utan tydlig stopppunkt, och man kan bara lägga till så många egenskaper som möjligt inom den tillgängliga tidsramen. Dessutom, när utvecklare ändrar koden när den verifieras måste de också uppdatera sina befintliga specifikationer, vilket leder till extra underhållsinsatser. Dessa faktorer kan göra formell verifiering till en skrämmande uppgift för vissa utvecklare som är tveksamma till att åta sig de extra omkostnaderna.

Och även om testning och formell verifiering kan förbättra kodkvaliteten när de används tillsammans, kräver båda (ibland liknande) beskrivningar av ett programs förväntade beteende i olika språk och format. Att skriva och underhålla dessa beskrivningar är arbetskrävande, och att upprätthålla två olika former av samma beskrivning kan kännas som dubbelarbete. Detta väcker följande fråga: Är det möjligt att beskriva det förväntade beteendet på ett sätt som utvecklare kan använda för både testning och verifiering?

Överbrygga gapet mellan testning och formell verifiering med symbolisk testning och Halmos

Symbolisk testning, praxis att köra tester med symboliska indata, är en effektiv formell verifieringsmetod som minskar specifikationsoverhead. Detta tillvägagångssätt möjliggör användning av samma testfall för både testning och formell verifiering. Till skillnad från traditionell testning, som verifierar att ett program fungerar korrekt för en begränsad uppsättning ingångar, kontrollerar symbolisk testning programmet för alla möjliga ingångar, därför kan ett program som klarar symboliska tester anses formellt verifierat.

Halmos är ett formellt verifieringsverktyg designat för symbolisk testning. Istället för att kräva separata specifikationer eller lära sig ett nytt språk använder Halmos befintliga test som formella specifikationer. Att köra tester genom Halmos kommer automatiskt att verifiera att de klarar alla möjliga indata, eller ge motexempel. Detta eliminerar inte bara behovet av ytterligare specifikationsskrivning, utan möjliggör också återanvändning av test skrivna för enhetstestning eller fuzzing, för formella verifieringsändamål.

Utvecklare har därför större flexibilitet att välja mellan en rad kvalitetssäkringsalternativ, inklusive enhetstestning, fuzzing och formell verifiering, beroende på deras nuvarande behov. Tester kan till exempel snabbt identifiera enkla misstag, möjligen med hjälp av en fuzzer som genererar slumpmässiga indata, och sedan kan Halmos ytterligare öka förtroendet för programmets korrekthet över alla ingångar.

Exempel: Testa isPowerOfTwo() fungera

Som ett exempel, överväg följande isPowerOfTwo() funktion, som avgör om ett givet tal är en potens av två. Denna funktion använder en algoritm för bitmanipulation för effektivitet, men det kan vara utmanande att bevisa dess riktighet, särskilt i de fall då inmatningen inte är en tvåpotens.

Föreställ dig följande test för isPowerOfTwo() funktion: den jämför funktionens faktiska utdata med den förväntade uteffekten för en given ingång. Detta är ett parameteriserat test (även känt som ett egenskapsbaserat test), vilket innebär att du enkelt kan köra det med olika ingångsvärden, eventuellt med fuzzing-verktyg som Foundry.

Du kan använda detta test för att undersöka isPowerOfTwo() funktion genom enhetstestning eller fuzz-testning, kör den med ett urval av ingångar. Tester som dessa kan inte formellt bevisa riktigheten av funktionen, eftersom det är beräkningsmässigt omöjligt att köra testet för alla möjliga indata.

Halmos tillåter dock utvecklare att återanvända dessa redan existerande tester för formell verifiering med bara lite extra ansträngning. Verktyget kontrollerar att tester godkänns för alla möjliga indata genom att utföra symbolisk exekvering av testet och sedan verifiera att påståendet aldrig kränks, (eller, om påståendet is kränksgenom att tillhandahålla ett motexempel). Detta innebär att om testet klarar Halmos, verifieras korrektheten av funktionen formellt, vilket innebär att algoritmen är korrekt implementerad och har korrekt översatts av kompilatorn till bytekod.

Begränsning: Avgränsad symbolisk utförande

Det är i allmänhet inte möjligt att utföra helautomatiska, fullständiga symboliska tester, eftersom detta skulle kräva att lösa problemet stoppa problemet, vilket är känt för att vara oavgörbara. En anledning till detta är att det ofta är omöjligt att automatiskt avgöra hur många gånger en loop ska iterera symboliskt. Som ett resultat är helautomatisk formell verifiering i allmänhet oavgjord.

Med tanke på dessa grundläggande begränsningar prioriterar Halmos automatisering framför fullständighet. För detta ändamål är Halmos utformad för att utföra avgränsade symboliska resonemang för obegränsade loopar (där antalet iterationer beror på programinmatningar) eller arrayer med variabel längd (inklusive strängar). Detta offrar viss fullständighet, men tillåter Halmos att undvika att kräva att användaren tillhandahåller ytterligare anteckningar som slinginvarianter.

Tänk till exempel på följande iterativa version av isPowerOfTwo() funktion, som har en obegränsad while-loop, där antalet loopiterationer bestäms av det minsta antal bitar som krävs för att representera ingångsnumret.

Halmos itererar symboliskt denna obundna loop endast upp till en specificerad gräns. Till exempel, om gränsen är satt till 3, kommer Halmos att iterera slingan högst 3 gånger och kommer inte att ta hänsyn till ingångsvärden som skulle få slingan att iterera mer än 3 gånger (dvs alla värden som är större än eller lika med 2^3 ). I det här speciella fallet skulle en inställning av gränsen till 256 eller högre tillåta Halmos att vara komplett.

Demo: Formell verifiering av ERC721A med Halmos

För att demonstrera Halmos funktioner använde vi den för att symboliskt testa och formellt verifiera ERC721A, en mycket gasoptimerad implementering av ERC721-standarden som möjliggör satsvis prägling till nästan samma kostnad som enstaka prägling. ERC721A innehåller flera innovativa optimeringar att uppnå denna effektivitet; till exempel kan gas sparas genom att fördröja uppdateringar av tokens ägandedata tills token överförs, inte vid tidpunkten för prägning. Detta kräver användning av komplexa datastrukturer och algoritmer för att effektivt hämta ägarinformation från den lata datastrukturen. Och även om denna optimering förbättrar gaseffektiviteten, ökar den också kodkomplexiteten och gör det utmanande att bevisa implementeringens korrekthet. Detta gör ERC721A till en bra kandidat för formell verifiering, eftersom det kan öka förtroendet för implementeringen och gynna potentiella användare.

Symboliska testegenskaper

Eftersom de befintliga testerna för ERC721A skrevs i JavaScript med Hardhat (som för närvarande inte stöds av Halmos), skrev vi nya test i Solidity för de viktigaste ingångsfunktionerna: mint(), burn()och transfer(). Dessa tester kontrollerade att varje funktion korrekt uppdaterar tokens ägande och saldo, och endast påverkar relevanta användare utan att ändra balansen eller ägandet för andra användare. Det senare är inte trivialt att bevisa på grund av användningen av den lata datastrukturalgoritmen i ERC721A. Till exempel kontrollerar följande test att transfer() funktionen uppdaterar ägandet av den angivna token korrekt:

Ett annat test kontrollerar att transfer() Funktionen ändrar inte balansen för andra adresser, vilket är svårt att bevisa som tidigare nämnt:

Verifieringsresultat

Vi genomförde ett verifieringsexperiment med Halmos på det smarta kontraktet ERC721A genom att skriva totalt 19 XNUMX tester. Testerna kördes genom Halmos med en loop-utrullningsgräns på 3, vilket tog 16 minuter att slutföra. Uppdelningen av verifieringstiden kan ses i tabellen nedan. Experimentet utfördes på en MacBook Pro med ett M1 Pro-chip och 16 GB minne.

Testa	Tid (er)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdOförändrad	1.40
testBurnOtherBalancePreservation	5.69
testBurnOtherOwnershipPreservation	189.70
testBurnOwnershipUpdate	3.81
testBurnRequirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintOtherOwnershipPreservation	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testTransferBalanceOförändrad	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdOförändrad	4.47
testTransferOtherBalancePreservation	19.57
testTransferOtherOwnershipPreservation	430.61
testTransferOwnershipUpdate	18.71
testTransferRequirements	149.18

Medan de flesta av testerna slutfördes på några sekunder, tog några av dem flera minuter. Dessa tidskrävande tester var utmanande att verifiera på grund av den komplexa karaktären hos de fall som skulle övervägas, och var nära relaterade till riktigheten av den lata datastrukturalgoritmen.

Sammantaget indikerar resultaten av detta experiment att Halmos effektivt kan verifiera riktigheten av smart kontraktskod. Det ger ökat förtroende för kodens integritet, trots det smarta kontraktets komplexitet och potentiella kantfall.

Experimentera med injicerade buggar

För att demonstrera effektiviteten av Halmos avgränsade resonemang använde vi det för att upptäcka buggar i en tidigare version av ERC721A-kontraktet. Den här versionen hade ett problem som misshandlade aritmetiskt överflöde och möjligen möjliggjorde batch-minting av ett stort antal tokens, vilket kunde bryta integriteten för den lata datastrukturen och resultera i att vissa användare förlorade sitt tokenägande (ett problem löst i den nuvarande versionen). Vi körde samma uppsättning av 19 tester för ERC721A på buggyversionen, och Halmos kunde hitta ett motexempel för egenskaperna hos mint() fungera. Specifikt gav Halmos ingångsvärden som ledde till exploateringsscenariot som beskrivs ovan. Resultaten av detta experiment indikerar att, trots dess ofullständighet, kan Halmos avgränsade resonemang vara ett effektivt sätt att upptäcka och förhindra exploateringsbara buggar i smarta kontrakt.

Relaterat arbete

Formella verifieringsverktyg för Ethereum smart kontrakt bytecode har utvecklats av olika team. Dessa verktyg, inklusive Halmos, kan användas för att säkerställa säkerheten och riktigheten av smarta kontrakt. Att jämföra och förstå de olika funktionerna, kapaciteten och begränsningarna hos dessa verktyg kan hjälpa utvecklare att välja det mest lämpliga för deras unika behov.

Medan Halmos är ett värdefullt tillägg till verktygsuppsättningen som är tillgänglig för smart kontraktsverifiering, är den tänkt att komplettera (inte ersätta) befintliga verktyg. Utvecklare kan kombinera Halmos med andra verktyg för att uppnå en högre grad av säkerhet i sina kontrakt. Nedan jämför vi Halmos med några utvalda formella verktyg som stöder EVM-bytekod.

• K är ett kraftfullt formellt verifieringsramverk som möjliggör deduktiv verifiering och interaktiv teorembevisning. Dess underliggande teori och implementering ger en hög nivå av uttrycksfullhet, vilket gör den lämplig för att verifiera komplexa program och algoritmer. Det bör dock noteras att K inte är utformad med stor tonvikt på automatiserad verifiering och saknar vissa automatiseringsfunktioner som kan kräva mer manuell ansträngning under verifieringsprocessen. För att använda K-ramverket är formella specifikationer skrivna på K-språket, som måste läras in före användning. Dess styrka är särskilt användbar för att verifiera komplexa system, som kan vara utmanande att analysera med hjälp av automatiserade resonemang.
• Certora är ett formellt verifieringsverktyg för smarta kontrakt som fokuserar på automatiserad verifiering och stöder gränsad modellkontroll, liknande Halmos. För att använda Certora måste utvecklare lära sig sitt nya språk, CVL, för att skriva specifikationer. Detta språk möjliggör en kortfattad beskrivning av många kritiska egenskaper genom kontraktsinvarianter, en funktion som Halmos för närvarande inte stöder. Trots att det är ett proprietärt verktyg med sluten källkod, tillhandahåller Certora robusta formella verifieringsverktyg, med pågående utveckling och bra användarstöd.
  
  Halmos, å andra sidan, är ett open source-verktyg som är mindre i skala och för närvarande saknar vissa funktioner som tillhandahålls av Certora, men det är tänkt att tjäna som en allmän nytta och är tänkt som en nischlösning för att snabbt verifiera smarta kontrakt utan behovet av omfattande installation och underhåll.
• HEVM är ett annat formellt verifieringsverktyg som liknar Halmos. Det var tidigare en del av DappTools, som är en föregångare till Foundry. Både HEVM och Halmos har funktionen att inte kräva en separat specifikation och kan symboliskt utföra befintliga tester för att identifiera påståendekränkningar. Detta tillåter användare att använda båda verktygen omväxlande eller köra dem parallellt för samma tester, vilket ger dem flera alternativ för symboliska tester.
  
  Det är värt att notera att, trots sina likheter, har HEVM och Halmos utvecklats oberoende av varandra och skiljer sig åt i sina implementeringsdetaljer; särskilt när det gäller optimeringar och symboliska resonemangsstrategier. Dessutom är HEVM skrivet i Haskell, medan Halmos är skrivet i Python, vilket ger exponering för det rika Python-ekosystemet. Att ha möjligheten att använda båda verktygen ger användarna mer flexibilitet och alternativ för att säkerställa säkerheten och riktigheten av smarta kontrakt.

Halmos är öppen källkod och för närvarande i sin betafas. Vi arbetar aktivt med nya pass och funktionalitet, inklusive Foundry-fuskkoder och flera andra viktiga användbarhetsfunktioner. Vi skulle uppskatta dina tankar om vilka funktioner som är viktigast och välkomnar all feedback, förslag och bidrag för att göra Halmos till ett bättre verktyg för alla.

**

De åsikter som uttrycks här är de från den individuella AH Capital Management, LLC (“a16z”) personal som citeras och är inte åsikterna från a16z eller dess dotterbolag. Viss information som finns här har erhållits från tredjepartskällor, inklusive från portföljbolag av fonder som förvaltas av a16z. Även om den är hämtad från källor som anses vara tillförlitliga, har a16z inte självständigt verifierat sådan information och gör inga utfästelser om den aktuella eller varaktiga riktigheten av informationen eller dess lämplighet för en given situation. Dessutom kan detta innehåll innehålla tredjepartsannonser; a16z har inte granskat sådana annonser och stöder inte något reklaminnehåll i dem.

Detta innehåll tillhandahålls endast i informationssyfte och bör inte litas på som juridisk rådgivning, affärs-, investerings- eller skatterådgivning. Du bör rådfråga dina egna rådgivare i dessa frågor. Hänvisningar till värdepapper eller digitala tillgångar är endast i illustrativt syfte och utgör inte en investeringsrekommendation eller erbjudande om att tillhandahålla investeringsrådgivningstjänster. Dessutom är detta innehåll inte riktat till eller avsett att användas av några investerare eller potentiella investerare, och får inte under några omständigheter lita på när man fattar ett beslut om att investera i någon fond som förvaltas av a16z. (Ett erbjudande om att investera i en a16z-fond kommer endast att göras av det privata emissionsmemorandumet, teckningsavtalet och annan relevant dokumentation för en sådan fond och bör läsas i sin helhet.) Alla investeringar eller portföljbolag som nämns, hänvisas till, eller beskrivna är inte representativa för alla investeringar i fordon som förvaltas av a16z, och det finns ingen garanti för att investeringarna kommer att vara lönsamma eller att andra investeringar som görs i framtiden kommer att ha liknande egenskaper eller resultat. En lista över investeringar gjorda av fonder som förvaltas av Andreessen Horowitz (exklusive investeringar för vilka emittenten inte har gett tillstånd för a16z att offentliggöra såväl som oanmälda investeringar i börsnoterade digitala tillgångar) finns tillgänglig på https://a16z.com/investments /.

Diagram och grafer som tillhandahålls i är endast i informationssyfte och bör inte litas på när man fattar investeringsbeslut. Tidigare resultat är inte en indikation på framtida resultat. Innehållet talar endast från det angivna datumet. Alla prognoser, uppskattningar, prognoser, mål, framtidsutsikter och/eller åsikter som uttrycks i detta material kan ändras utan föregående meddelande och kan skilja sig åt eller strida mot åsikter som uttrycks av andra. Se https://a16z.com/disclosures för ytterligare viktig information.