Symbolsk testing med Halmos: Utnyttelse av eksisterende tester for formell verifisering

Formell verifisering - prosessen med å bruke matematiske metoder for å "inspisere" et program eller en smart kontrakt på tvers av et hvilket som helst antall innganger - blir generelt sett på som det mer konsise, mer omfattende alternativet til tradisjonell testing for å skrive høyere kvalitet og sikrere kode. Men i virkeligheten er formell verifisering en åpen og interaktiv prosess. På samme måte som enhetstesting, må utviklere dynamisk definere og legge på formelle spesifikasjoner, iterere på tilnærmingen deres etter hvert som koden og analysene deres utvikler seg. Videre er formell verifisering bare så effektiv som spesifikasjonene, noe som kan være tidkrevende å skrive (og ofte kommer med en bratt læringskurve). 

For mange utviklere som synes prosessen er skremmende, er enhetstester ofte den mer kostnadseffektive og tidseffektive veien for å finne ut om et program er korrekt. Formell verifikasjon er i praksis ikke et mer omfattende alternativ til enhetstesting, men et komplementært alternativ. Disse prosessene har forskjellige styrker og begrensninger, og gir enda større sikkerhet når de brukes sammen. Utviklere vil alltid måtte skrive enhetstester - så hva om vi kunne bruke de samme egenskapene for formell verifisering?

Halmos, vårt formelle verifiseringsverktøy med åpen kildekode, lar utviklere gjenbruk de samme egenskapene skrevet for enhetstester for formelle spesifikasjoner gjennom symbolsk testing. I stedet for å måtte lage et robust sett med egenskaper fra starten av, kan utviklere unngå duplikativt arbeid og forbedre testene noen få spesifikasjoner om gangen uten å starte fra bunnen av. Vi utviklet dette verktøyet for bruk, sammen med andre i den formelle verifiseringsprosessen, som en påkjøring til formell verifisering; utviklere kan starte med noen få analyser med minimal innsats, før de legger til flere senere i prosessen.

I dette innlegget dekker vi utfordringene med formell verifisering, og potensialet for å bygge bro mellom enhetstesting og formell verifisering med symbolsk testing. Vi går deretter gjennom en demo av Halmos ved å bruke eksisterende smart kontraktskode, og tar en rask titt på andre formelle verifiseringsverktøy (mange åpen kildekode) tilgjengelig for utviklere.

Formell verifisering kontra testing

Formell bekreftelse - generelt foretrukket av blockchain-utviklere for sin strenghet og omfattendehet - er prosessen med å bevise riktigheten til et program ved å verifisere at det tilfredsstiller visse korrekthetsegenskaper. Egenskapene, som er spesifikke for programmet, er vanligvis gitt eksternt og uttrykt ved hjelp av et formelt språk eller notasjon som støttes av verifiseringsverktøyet som brukes. Utviklere oppfatter ofte formell verifisering som en trykknappløsning for automatisk testing av egenskaper på tvers av alle mulige scenarier, men i virkeligheten kan formell verifisering være en arbeidskrevende og svært interaktiv prosess.

Som formell verifisering involverer enhetstesting å evaluere om et program fungerer som forventet; testing sjekker imidlertid bare programmets oppførsel for noen innganger, mens formell verifisering kan sjekke det for alle mulige innganger. Både testing og formell verifisering krever en beskrivelse av forventet oppførsel av programmet (med testtilfeller brukt i testing og formelle spesifikasjoner brukt i formell verifisering). Men når de brukes sammen, kan de gi en mer grundig undersøkelse av et program. Testing, for eksempel, er effektivt for å finne enkle feil og feil, men er generelt raskere og enklere å utføre. Formell verifisering, selv om den er mer tungvint å bruke, er kraftig nok til å bevise fraværet av feil eller avsløre subtile feil som er lett å gå glipp av i testing eller kodevurderinger.

Spesifikasjon overhead

En av hovedutfordringene med formell verifisering er overheaden med å skrive og vedlikeholde formelle spesifikasjoner. Denne prosessen involverer ofte den tidkrevende oppgaven med å manuelt skrive spesifikasjonene ved å bruke et spesialisert språk (som mange utviklere må lære seg først). Prosessen er også inkrementell, og starter vanligvis med å skrive enkle egenskaper og verifisere dem først, og deretter gradvis legge til mer komplekse egenskaper på toppen. I likhet med testing er det en åpen prosess, uten noe klart stopppunkt, og man kan bare legge til så mange egenskaper som mulig innenfor den tilgjengelige tidsrammen. I tillegg, når utviklere endrer koden mens den blir verifisert, må de også oppdatere sine eksisterende spesifikasjoner, noe som fører til ekstra vedlikeholdsinnsats. Disse faktorene kan gjøre formell verifisering til en skremmende oppgave for noen utviklere som nøler med å forplikte seg til de ekstra kostnadene.

Og selv om testing og formell verifisering kan forbedre kodekvaliteten når de brukes sammen, krever begge (noen ganger lignende) beskrivelser av et programs forventede oppførsel på forskjellige språk og formater. Å skrive og vedlikeholde disse beskrivelsene er arbeidskrevende, og å opprettholde to forskjellige former for samme beskrivelse kan føles som duplisert innsats. Dette reiser følgende spørsmål: Er det mulig å beskrive forventet oppførsel på en måte som utviklere kan bruke til både testing og verifisering?

Bygge bro mellom testing og formell verifisering med symbolsk testing og Halmos

Symbolsk testing, praksisen med å kjøre tester med symbolske innganger, er en effektiv formell verifiseringsmetode som reduserer spesifikasjonskostnader. Denne tilnærmingen muliggjør bruk av de samme testtilfellene for både testing og formell verifisering. I motsetning til tradisjonell testing, som verifiserer at et program fungerer riktig for et begrenset sett med innganger, sjekker symbolsk testing programmet for alle mulige innganger, og derfor kan et program som består symbolsk testing anses som formelt verifisert.

Halmos er et formelt verifiseringsverktøy designet for symbolsk testing. I stedet for å kreve separate spesifikasjoner eller lære et nytt språk, bruker Halmos eksisterende tester som formelle spesifikasjoner. Å kjøre tester gjennom Halmos vil automatisk bekrefte at de består for alle mulige innganger, eller gi moteksempler. Dette eliminerer ikke bare behovet for ytterligere spesifikasjonsskriving, men tillater også gjenbruk av tester skrevet for enhetstesting eller fuzzing, for formelle verifikasjonsformål.

Utviklere har dermed større fleksibilitet til å velge mellom en rekke kvalitetssikringsalternativer, inkludert enhetstesting, fuzzing og formell verifisering, avhengig av deres nåværende behov. For eksempel kan tester raskt identifisere enkle feil, muligens ved hjelp av en fuzzer som genererer tilfeldige innganger, og deretter kan Halmos ytterligere øke tilliten til programmets korrekthet på tvers av alle innganger.

Eksempel: Testing av isPowerOfTwo() funksjon

Tenk på følgende som et eksempel isPowerOfTwo() funksjon, som bestemmer om et gitt tall er en potens av to. Denne funksjonen bruker en bitmanipulasjonsalgoritme for effektivitet, men det kan være utfordrende å bevise at det er korrekt, spesielt i tilfellet hvor input ikke er en potens av to.

Tenk deg følgende test for isPowerOfTwo() funksjon: den sammenligner den faktiske utgangen av funksjonen med den forventede utgangen for en gitt inngang. Dette er en parameterisert test (også kjent som en egenskapsbasert test), noe som betyr at du enkelt kan kjøre den med forskjellige inngangsverdier, muligens med uklare verktøy som Foundry.

Du kan bruke denne testen til å undersøke isPowerOfTwo() fungerer gjennom enhetstesting eller fuzz-testing, og kjører den med et utvalg innganger. Tester som disse kan ikke formelt bevise riktigheten av funksjonen, da det er beregningsmessig umulig å kjøre testen for alle mulige input.

Halmos lar imidlertid utviklere gjenbruke disse eksisterende testene for formell verifisering med bare litt ekstra innsats. Verktøyet sjekker at testene består for alle mulige innganger ved å utføre symbolsk utførelse av testen og deretter verifisere at påstanden aldri blir krenket, (eller, hvis påstanden is krenket, ved å gi et moteksempel). Dette betyr at hvis testen består Halmos, blir riktigheten av funksjonen formelt verifisert, noe som betyr at algoritmen er korrekt implementert og er nøyaktig oversatt av kompilatoren til bytekode.

Begrensning: Avgrenset symbolsk utførelse

Det er generelt ikke mulig å utføre helautomatisk, fullstendig symbolsk testing, da dette vil kreve å løse problemet stanseproblem, som er kjent for å være uavgjørlig. En grunn til dette er at det ofte er umulig å bestemme automatisk hvor mange ganger en løkke skal iterere symbolsk. Som et resultat er helautomatisk formell verifisering generelt uavgjort.

Gitt disse grunnleggende begrensningene, prioriterer Halmos automatisering fremfor fullstendighet. For dette formål er Halmos designet for å utføre avgrensede symbolske resonnementer for ubegrensede løkker (hvor antall iterasjoner avhenger av programinndata) eller arrayer med variabel lengde (inkludert strenger). Dette ofrer en viss fullstendighet, men lar Halmos unngå å kreve at brukeren oppgir ytterligere merknader som sløyfeinvarianter.

Tenk for eksempel på følgende iterative versjon av isPowerOfTwo() funksjon, som har en ubegrenset while-løkke, hvor antall loop-iterasjoner bestemmes av minimum antall biter som kreves for å representere inngangsnummeret.

Halmos gjentar symbolsk denne ubegrensede løkken bare opp til en spesifisert grense. For eksempel, hvis grensen er satt til 3, vil Halmos iterere løkken maksimalt 3 ganger og vil ikke vurdere inngangsverdier som vil få løkken til å iterere mer enn 3 ganger (dvs. alle verdier større enn eller lik 2^3 ). I dette spesielle tilfellet vil å sette grensen til 256 eller høyere tillate Halmos å være komplett.

Demo: Formell verifisering av ERC721A med Halmos

For å demonstrere egenskapene til Halmos brukte vi den til å symbolsk teste og formelt verifisere ERC721A, en svært gassoptimalisert implementering av ERC721-standarden som gjør det mulig for batch-preging til nesten samme pris som enkeltpreging. ERC721A inkluderer flere innovative optimaliseringer for å oppnå denne effektiviteten; for eksempel kan gass spares ved å utsette oppdateringer av token-eierskapsdata til tokenet er overført, ikke på tidspunktet for preging. Dette krever bruk av komplekse datastrukturer og algoritmer for å effektivt hente eierskapsinformasjon fra den late datastrukturen. Og selv om denne optimaliseringen forbedrer gasseffektiviteten, øker den også kodekompleksiteten og gjør det utfordrende å bevise implementeringens korrekthet. Dette gjør ERC721A til en god kandidat for formell verifisering, da det kan øke tilliten til implementeringen og komme potensielle brukere til gode.

Symbolske testegenskaper

Siden de eksisterende testene for ERC721A ble skrevet i JavaScript med Hardhat (som for øyeblikket ikke støttes av Halmos), skrev vi nye tester i Solidity for hovedinngangsfunksjonene: mint(), burn()og transfer(). Disse testene sjekket at hver funksjon oppdaterer tokeneierskap og balanse på riktig måte, og kun påvirker de relevante brukerne uten å endre balansen eller eierskapet til andre brukere. Sistnevnte er ikke-trivielt å bevise på grunn av bruken av den late datastrukturalgoritmen i ERC721A. Følgende test kontrollerer for eksempel at transfer() funksjonen oppdaterer eierskapet til det angitte tokenet på riktig måte:

En annen test sjekker at transfer() funksjon endrer ikke balansen for andre adresser, noe som er utfordrende å bevise som nevnt tidligere:

Bekreftelsesresultater

Vi utførte et verifiseringseksperiment med Halmos på ERC721A smart kontrakt ved å skrive totalt 19 XNUMX tester. Testene ble kjørt gjennom Halmos med en løkkeutrullingsgrense på 3, som tok 16 minutter å fullføre. Fordelingen av verifikasjonstiden kan ses i tabellen nedenfor. Eksperimentet ble utført på en MacBook Pro med en M1 Pro-brikke og 16 GB minne.

Test	Tid (er)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUendret	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
testTransferBalanceUendret	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdUendret	4.47
testTransferOtherBalancePreservation	19.57
testTransferOtherOwnershipPreservation	430.61
testTransferOwnershipUpdate	18.71
testTransferkrav	149.18

Mens de fleste av testene ble fullført i løpet av sekunder, tok noen få av dem flere minutter. Disse tidkrevende testene var utfordrende å verifisere på grunn av den komplekse karakteren til sakene som skulle vurderes, og var nært knyttet til riktigheten av den late datastrukturalgoritmen.

Samlet sett indikerer resultatene av dette eksperimentet at Halmos effektivt er i stand til å verifisere riktigheten av smart kontraktskode. Det gir økt tillit til kodens integritet, til tross for kompleksiteten og potensielle kanttilfellene til den smarte kontrakten.

Eksperimenter med injiserte insekter

For å demonstrere effektiviteten til Halmos avgrensede resonnement, brukte vi den til å oppdage feil i en tidligere versjon av ERC721A-kontrakten. Denne versjonen hadde et problem som mishandlet aritmetisk overløp og muligens muliggjorde batch-utsetting av et stort antall tokens, noe som kunne bryte integriteten til den late datastrukturen og føre til at noen brukere mistet token-eierskapet (et problem løst i gjeldende versjon). Vi kjørte det samme settet med 19 tester for ERC721A på buggy-versjonen, og Halmos var i stand til å finne et moteksempel for egenskapene til mint() funksjon. Nærmere bestemt ga Halmos inngangsverdier som førte til utnyttelsesscenarioet beskrevet ovenfor. Resultatene av dette eksperimentet indikerer at til tross for at det er ufullstendig, kan Halmos avgrensede resonnement være en effektiv måte å oppdage og forhindre utnyttbare feil i smarte kontrakter.

Relatert arbeid

Formelle verifiseringsverktøy for Ethereum smart kontraktsbytekode er utviklet av forskjellige team. Disse verktøyene, inkludert Halmos, kan brukes til å sikre sikkerheten og riktigheten til smarte kontrakter. Å sammenligne og forstå de forskjellige funksjonene, egenskapene og begrensningene til disse verktøyene kan hjelpe utviklere å velge den mest passende for deres unike behov.

Mens Halmos er et verdifullt tillegg til verktøysettet som er tilgjengelig for smart kontraktsverifisering, er det ment å komplementere (ikke erstatte) eksisterende verktøy. Utviklere kan kombinere Halmos med andre verktøy for å oppnå en høyere grad av sikkerhet i kontraktene sine. Nedenfor sammenligner vi Halmos med noen få utvalgte formelle verktøy som støtter EVM-bytekode.

• K er et kraftig formelt verifikasjonsrammeverk som muliggjør deduktiv verifisering og interaktiv teorembevis. Dens underliggende teori og implementering gir et høyt nivå av uttrykksevne, noe som gjør den egnet for å verifisere komplekse programmer og algoritmer. Det skal imidlertid bemerkes at K ikke er designet med stor vekt på automatisert verifisering og mangler visse automatiseringsfunksjoner som kan kreve mer manuell innsats under verifiseringsprosessen. For å bruke K-rammeverket, er formelle spesifikasjoner skrevet på K-språket, som må læres før bruk. Styrken er spesielt nyttig for å verifisere komplekse systemer, som kan være utfordrende å analysere ved hjelp av automatisert resonnement.
• Certora er et formelt verifiseringsverktøy for smarte kontrakter som fokuserer på automatisert verifisering og støtter avgrenset modellsjekking, i likhet med Halmos. For å bruke Certora må utviklerne lære det nye språket sitt, CVL, for å skrive spesifikasjoner. Dette språket tillater en kortfattet beskrivelse av mange kritiske egenskaper gjennom kontraktinvarianter, en funksjon som Halmos foreløpig ikke støtter. Til tross for at det er et proprietært verktøy med lukket kilde, tilbyr Certora robuste formelle verifiseringsverktøy, med kontinuerlig utvikling og god brukerstøtte.
  
  Halmos, derimot, er et åpen kildekodeverktøy som er mindre i skala og mangler noen funksjoner levert av Certora, men det er ment å tjene som et offentlig gode og er ment som en nisjeløsning for raskt å verifisere smarte kontrakter uten behovet for omfattende oppsett og vedlikehold.
• HEVM er et annet formelt verifiseringsverktøy som ligner på Halmos. Det var tidligere en del av DappTools, som er en forløper for Foundry. Både HEVM og Halmos har funksjonen til å ikke kreve en egen spesifikasjon og kan symbolsk utføre eksisterende tester for å identifisere påstandsbrudd. Dette lar brukere bruke begge verktøyene om hverandre eller kjøre dem parallelt for de samme testene, og gir dem flere alternativer for symbolsk testing.
  
  Det er verdt å merke seg at til tross for likhetene deres, har HEVM og Halmos blitt utviklet uavhengig av hverandre og er forskjellige i implementeringsdetaljer; spesielt når det gjelder optimaliseringer og symbolske resonnementstrategier. I tillegg er HEVM skrevet i Haskell, mens Halmos er skrevet i Python, noe som gir eksponering for det rike Python-økosystemet. Å ha muligheten til å bruke begge verktøyene gir brukerne mer fleksibilitet og muligheter for å sikre sikkerheten og riktigheten til smarte kontrakter.

Halmos er åpen kildekode, og for øyeblikket i betafasen. Vi jobber aktivt med nye egenskaper og funksjonalitet, inkludert Foundry-juksekoder og flere andre viktige brukervennlighetsfunksjoner. Vi vil sette stor pris på dine tanker om hvilke funksjoner som er viktigst, og tar gjerne imot tilbakemeldinger, forslag og bidrag for å gjøre Halmos til et bedre verktøy for alle.

**

Synspunktene som er uttrykt her, er de fra individuelle AH Capital Management, LLC (“a16z”) personell som er sitert og er ikke synspunktene til a16z eller dets tilknyttede selskaper. Visse opplysninger her er innhentet fra tredjepartskilder, inkludert fra porteføljeselskaper av fond forvaltet av a16z. Selv om a16z er hentet fra kilder som antas å være pålitelige, har ikke a16z uavhengig verifisert slik informasjon og gir ingen representasjoner om den nåværende eller varige nøyaktigheten til informasjonen eller dens hensiktsmessighet for en gitt situasjon. I tillegg kan dette innholdet inkludere tredjepartsannonser; aXNUMXz har ikke vurdert slike annonser og støtter ikke noe reklameinnhold som finnes deri.

Dette innholdet er kun gitt for informasjonsformål, og bør ikke stoles på som juridisk, forretningsmessig, investerings- eller skatterådgivning. Du bør rådføre deg med dine egne rådgivere om disse sakene. Referanser til verdipapirer eller digitale eiendeler er kun for illustrasjonsformål, og utgjør ikke en investeringsanbefaling eller tilbud om å tilby investeringsrådgivningstjenester. Videre er dette innholdet ikke rettet mot eller ment for bruk av noen investorer eller potensielle investorer, og kan ikke under noen omstendigheter stoles på når du tar en beslutning om å investere i et fond som forvaltes av a16z. (Et tilbud om å investere i et a16z-fond vil kun gis av det private emisjonsmemorandumet, tegningsavtalen og annen relevant dokumentasjon for et slikt fond og bør leses i sin helhet.) Eventuelle investeringer eller porteføljeselskaper nevnt, referert til, eller beskrevet er ikke representative for alle investeringer i kjøretøy forvaltet av a16z, og det kan ikke gis noen garanti for at investeringene vil være lønnsomme eller at andre investeringer som gjøres i fremtiden vil ha lignende egenskaper eller resultater. En liste over investeringer foretatt av fond forvaltet av Andreessen Horowitz (unntatt investeringer som utstederen ikke har gitt tillatelse til at a16z kan offentliggjøre så vel som uanmeldte investeringer i børsnoterte digitale eiendeler) er tilgjengelig på https://a16z.com/investments /.

Diagrammer og grafer gitt i er kun for informasjonsformål og bør ikke stoles på når du tar investeringsbeslutninger. Tidligere resultater er ikke en indikasjon på fremtidige resultater. Innholdet taler kun fra den angitte datoen. Eventuelle anslag, estimater, prognoser, mål, prospekter og/eller meninger uttrykt i dette materialet kan endres uten varsel og kan avvike eller være i strid med meninger uttrykt av andre. Vennligst se https://a16z.com/disclosures for ytterligere viktig informasjon.