NyheterUtvecklareFöretagBlockchain förklaradeHändelser och konferenserPressNyhetsbrev

Contents

0.1 Prenumerera på vårt nyhetsbrev.

1 Formellt verifiera Ethereum 2.0 fas 0-specifikationerna

Prenumerera på vårt nyhetsbrev.

E-postadress

Vi respekterar din integritet

HemBlogBlockchain utveckling

Formellt verifiera Ethereum 2.0 fas 0-specifikationerna

En uppdatering från ConsenSys R&D om deras ansträngningar för att ge trovärdighet till Beacon Chain och kärnan i Eth2. av Franck Cassez 10 augusti 2020 Upplagt den 10 augusti 2020

Teamet för automatiserad verifiering på ConsenSys R&D har arbetat med en formell specifikation och verifiering av Beacon Chain i några månader. Vi är glada att kunna rapportera att många framsteg har gjorts och även om de ännu inte är klara har vi lyckats utvecklas en solid och formellt verifierad kärna från Beacon Chain. För första gången ger vårt arbete en oöverträffad nivå av tillförlitlighet för kärnan i Eth2.0-infrastrukturen.

Metodik

Verifiering kontra testning

Vi använde prisbelönt verifieringsmedvetet programmeringsspråk Dafny att skriva en formell (funktionell och logisk) Specifikation för varje Beacon Chain-funktion, en genomförande för varje funktion, och a bevis att implementeringen överensstämmer med specifikationen. Med andra ord har vi matematiskt verifierat frånvaron av buggar. De implementeringar som vi så småningom har visat sig vara korrekta baseras på de officiella Eth2.0-specifikationerna med förbehållet att vi har fixat och rapporterat några fel och inkonsekvenser.

Vår metodik skiljer sig från att testa som vi matematiskt bevisa funktionernas överensstämmelse med deras specifikationer, för Allt ingångar. Testning kan inte sträcka sig över oändligt många ingångar och kan som en följd upptäcka buggar men inte bevisa frånvaron av buggar.

Och det bästa är att vi inte behöver publicera en uppsats eller granska bevisen. Bevisen är en del av kodbasen och skrivs som program. Ja, i Dafny kan du skriva ett bevis som ett utvecklarvänligt program. Även bevis kontrolleras mekaniskt av en teoremprover och lämnar inget utrymme för ofullständiga eller felaktiga bevis.

Egenskaper vi har bevisat

Egenskaperna sträcker sig från frånvaron av aritmetik under / överflöd och index utanför gränserna, överensstämmelse för varje funktion till logiska (första ordningens logik) före / efter villkor (merkelise-exempel här), till mer komplexa som involverar funktionskompositioner. Till exempel har vi följande SSZ: s egendom Serialisera / Deserialisera funktioner: för varje objekt x, Avserialisera (Serialisera (x)) = x, dvs. avserialisera ett serieobjekt returnerar originalobjektet. Vi har också etablerat en antal invarianter, och använde dem för att bevisa att kärnverksamheten i Beacon Chain och ForkChoice (state_transition, on_block) faktiskt bygg en kedja av block: för varje block b i butiken bildar förfäderna till b en slutlig helt ordnad sekvens som leder till genesblocket, vilket är den huvudsakliga egenskapen hos en blockchain!

Fördelarna med formell verifiering

Varje formell metodist skulle insistera på att verifiering är en säkerhetsmetod. Här är exakt hur denna metod säkerställer en säker och pålitlig infrastruktur för Ethereum 2.0.

Funktionell specifikation

Först har vi lyft de officiella Eth2.0-specifikationerna till a formell logisk och funktionell specifikation. För varje funktion definierar vi formellt vad funktionen förväntas beräkna, inte hur. Detta ger språkagnostiska utvecklarvänliga referensspecifikationer som kan användas för att utveckla säkrare implementeringar, med mindre ansträngning.

Modularitet

För det andra är våra specifikationer, implementeringar och bevisarkitektur modul-. Som ett resultat kan vi enkelt experimentera med nya implementeringar (t.ex. optimeringar) och kontrollera deras inverkan på det totala systemet. Tänk på ett smart hack för att implementera en funktion? Ändra implementeringen och be Dafny att kontrollera att den fortfarande överensstämmer med specifikationen. Om den gör det påverkas inte bevisen för de komponenter som använder den här funktionen.

Körbarhet

För det tredje är våra implementeringar det körbar. Vi kan sammanställa och köra ett Dafny-program. Ännu bättre kan du automatiskt generera kod på några populära programmeringsspråk som C #, Go (och snart Java) från Dafny-koden. Detta kan användas för att komplettera befintliga kodbaser eller för att generera certifierade tester. Implementationen som ska testas kan använda våra bevisade korrekta funktioner för att beräkna det förväntade resultatet av ett test och kontrollera det mot sitt eget resultat.

Allt på ett enda språk

Sist men inte minst är vår kodbas fristående. Den innehåller specifikationer, implementeringar, dokumentationer och bevis, allt på ett enda, läsbart, enkelt och semantiskt väldefinierat programmeringsspråk.

Frågor och överväganden

Vad sägs om verifieringsmotorns sundhet?

Du kanske undrar, “vad händer om Dafny-kompilatorn / verifieraren är buggy?” Vi vet faktiskt att Dafny är buggy (dafny repo problem), men vi litar inte på frånvaron av buggar i Dafny. Vi litar på att Dafny (och dess verifieringsmotor) är ljud. Sundhet betyder att när Dafny rapporterar att bevis är korrekta, är de verkligen korrekta.

Vad händer om specifikationen vi har skrivit inte är rätt?

I det här fallet skulle vi bevisa överensstämmelse med fel krav. Ja, detta kan hända och det finns ingen silverkula för att lösa problemet. Som vi nämnde tidigare är Dafny dock körbar. Detta gör att vi kan köra koden och få lite förtroende för att våra specifikationer är de rätta. Och våra specifikationer är skrivna i första ordningens logik utan utrymme för tvist om innebörden, så om du märker ett problem, låt oss veta så fixar vi det.

Vad händer om Dafny inte kan bevisa att en implementering överensstämmer med en specifikation?

Detta kan hända, men i det här fallet har Dafny några feedbackmekanismer för att undersöka vilka steg i ett bevis som inte kan verifieras. Och hittills har vi alltid lyckats skapa bevis som Dafny automatiskt kan kontrollera.

Vi välkomnar din feedback, så kolla in vårt eth2.0-dafny-arkiv. Vi har varit glada att se utvecklingen av Ethereum 2.0 nå sina senaste testnät milstolpar, och vi ser fram emot att arbeta med team över hela ekosystemet för att säkerställa att nästa fas i nätverket bygger på en bunnsolid grund.

Bekräftelse: Tack till mina lagkamrater Joanne Fuller, Roberto Saltini (Automated Verification team), Nicolas Liochon och till Avery Erwin för kommentarer om en preliminär version av detta inlägg.

Håll dig uppdaterad om Ethereum 2.0

Prenumerera på ConsenSys nyhetsbrev för att få de senaste Eth2-nyheterna direkt till din inkorg. Prenumerera Ethereum 2.0Forskning och utvecklingSäkerhetNyhetsbrevPrenumerera på vårt nyhetsbrev för de senaste Ethereum-nyheterna, företagslösningar, utvecklarresurser och mer.E-postadressExklusivt innehållWebinar