Farväl buggar? Hur formell verifiering skulle kunna bekräfta smarta kontrakt

The Thinning (Juni 2019).

Anonim

Som ett sätt att eliminera buggar i high- risk kod, en typ av programvara programmering som kallas formell verifiering gör sin väg in i blockchain världen.

Enkelt, formell verifiering använder matematik för att specificera och analysera ett program för fel i logiken. På grund av den aktuella tiden och kostnaden är den formella verifieringen bäst reserverad för situationer där mänskligt liv eller stora summor pengar står på spel.

För närvarande används formell verifiering för att verifiera korrektheten av högriskkoden vid transport, militär och kryptografi. Chipföretag använder det för att befästa algoritmer innan de inbäddas i kisel. Och banker använder den för att utveckla finansiella algoritmer.

Tillämpad för blockchain-teknik kan formell kontroll verka för att självförverkande transaktioner som kallas smarta kontrakt kommer att fungera som avsedda, vilket eliminerar några av de fel och ekonomiska förluster som kommer till följd av kodningsfel.

Bara i år svarade buggar i Ethereums paritetsplånbok för 180 miljoner dollar i förluster. Förra året gjorde en bugg i en virtuell organisation, känd som The DAO, en hackare att sipponera 50 miljoner dollar från Ethereums smarta kontrakt.

Plattformar som Cardano och Tezos arbetar redan på smarta kontraktsspråk som är speciellt utformade för att underlätta formell verifiering. Ethereum arbetar också med att formellt verifiera sina smarta kontrakt.

Men vad är formell verifiering? Hur fungerar det? Och varför är mjukvaran så svår att få rätt i första hand?

Till Err är mänsklig

Programvaran är i sig oförsonlig. Om du bygger en byggnad kan du lämna ut en spik eller en skruv, och strukturen står fortfarande. Men när det gäller programvara kan någonting så enkelt som ett enda typsnitt orsaka att hela programmet slutar fungera.

"Programmeringsspråk är oerhört kraftfulla", förklarade Gerard Holzmann, tidigare ledande forskare vid NASA, i en intervju med Bitcoin Magazine . "Som programmerare måste du ta itu med mycket detalj, och om du inte får varje detalj rätt har det någon effekt. "

Det traditionella sättet att få rätt program är att testa. När du har skrivit en algoritm matar du in en variabel och kontrollerar om den ger tillbaka den korrekta utgången. Men hur testar du varje enskild ingång? Du kan inte. Det finns för många att testa, och det kan finnas fel som lurar i de fall du inte testar.

"Det finns så många möjliga avrättningar som verkligen, när du testar eller utför, klipper du bara ytan på vad som är möjligt," sa Holzmann.

Sätt ett annat sätt, testning söker bara efter förekomst av fel, inte frånvaron av fel, och ett litet misstag kan få förödande resultat.

"Om du misslyckas av ett system, som Fukushima och Three Mile Island, och titta på händelsens följd som ledde till det misslyckandet, är det alltid fascinerande eftersom det finns så många saker som ingen kunde ha förutsagt det skulle hända i ett visst boende, säger Holzmann."Samma som i mjukvara; så många saker kan hända. "

I motsats till, istället för att testa en situation i taget, är formell verifiering ett sätt att testa att ett program fungerar i alla situationer. Vad du bryr dig om är om logiken är sant, och det bästa sättet att kontrollera logiken är med en dator.

"En formalism för mig har det syfte att du kan räkna med saker och det mest användbara sättet att räkna med saker är om du kan programmera en maskin för att göra resonemanget för dig", säger Holzmann.

Skapa en plan

Generellt är det första steget i formell verifiering att skapa en matematisk modell. Matematiken som behövs är inte komplicerad; Det är bara grundläggande logik som skrivits upp i ett så kallat "formellt språk" som kan kontrolleras av maskinen.

Vanligtvis börjar processen med att specificera en modell med en intressent som förstår vad systemet behöver göra. Vid medicinsk utrustning kan intressenten vara en läkare; i fallet med ett smart kontrakt kan det vara en advokat eller en bankir eller båda.

Arbetet med en intressent är att förmedla informationen i huvudet till en kravtekniker som samlar in den informationen och skapar modellen. Processen börjar informellt med diskussioner och abstraktioner, men slutar formellt med en exakt matematisk specifikation.

Det här är inte lätt. Det är en tidskrävande iterativ process som kan ta flera månader, beroende på situationen, men det ger ofta en klarhet till en situation som inte var där förut eftersom det tvingar programmerare att tänka djupt om hur en mjukvara fungerar.

"Du kan tänka på det som lagar och förordningar", säger Andreas Zeller, professor i mjukvaruutveckling vid Saarlands universitet i Saarbruecken, Tyskland, som liknar att skapa en formell specifikation för att utveckla en plan för en byggnad.

"Du förfina reglerna," berättade han Bitcoin Magazine . "Men om du inte har regler i första hand, kraschar din byggnad, och det är när du inser att du hade bättre gjort en plan. "

Kontrollera logiken

När en modell har angivits är nästa steg att verifiera modellens logik med bevis. Detta är ett kritiskt steg i processen. "Om du inte har ett bevis har du ingen garanti för att modellen, som den är, kommer att fungera," förklarade Zeller.

Men eftersom du måste uttrycka varje logiskt steg kan bevis vara oerhört lång och komplex. I det förflutna gjorde detta formella verifieringen besvärligt svårt. Även det enklaste uttalandet kan kräva dussintals stämningar och lemmor.

Lyckligtvis, idag använder många formella system automatiserade teoremprövare, som Coq, Isabelle eller Metamath, som kan kontrollera eller till och med delvis konstruera ett formellt bevis.

När en modell har visat sig fungera, bygger nästa steg ditt program. Men du måste fortfarande se till att programvaran du bygger överensstämmer med specifikationen.

Här är funktionella programmeringsspråk som ML, Haskell, OCaml eller F # in i bilden. Eftersom dessa språk är närmare algebra i deras uttryck, är de en bättre match för formell verifiering än språk som C, Java eller JavaScript.

Därför är Tezos skrivet i OCaml och Cardano är skrivet i Haskell, så ändringar i protokollet är enklare att formellt verifiera. (En formell specifikation för Ouroboros Praos, nästa generation av konsensusalgoritmen som driver Cardano, finns redan i verk.) På samma sätt bygger Tezos smarta kontraktsspråk Michelson på OCaml; Cardans smarta kontraktsspråk Plutus är baserat på Haskell.

Fördelar och nackdelar

På den positiva sidan tillåter den formella verifieringen datorerna större försäkringar när det gäller att utveckla programvara. På den negativa sidan kan de formella metoderna vara ett tidskrävande och kostsamt företag för att utveckla koden på grund av den inblandade rigor.

På grund av detta används formella metoder för att garantera mindre byggstenar av kod som återanvändas om och om igen. Du skulle inte använda det för att säga ett helt operativsystem, men bara de delar av ett system som kräver högsta säkerhets- eller säkerhetsföreskrifter.

Naturligtvis kommer någon typ av säkerhet till en kostnad. Frågan är hur mycket säkerhet kommer att blockchain och smarta kontraktsutvecklare är villiga att betala för?

Om du vill ha något som är felfritt, "hade du bättre varit beredd att spendera tiotalshundratusentals dollar för människor som kommer att ge ett fullständigt bevis", varnade Zeller.

Å andra sidan, för smarta avtal som säkrar tiotals miljoner dollar i fonder kan dessa kostnader vara värda det. Titta på det på ett annat sätt, i en konkurrensutsatt miljö kan formell kontroll göra smarta avtal mer tilltalande för konsumenten.

Om du till exempel hade valt att överlåta dina pengar till ett smart kontrakt som formellt verifierats mot en som inte har valt, vilken skulle du välja?

___________

Tack till Tim Menzies, professor i datavetenskap vid North Carolina University och Brighten Godfrey, medgrundare och CTO på Veriflow, och Automated Software Engineering 2017.