NewsDevelopersEnterpriseBlockchain ExplainedEvents and ConferencesPressButlletins informatius

Subscriu-te al nostre butlletí.

Correu electrònic

Respectem la vostra privadesa

IniciBlogBlockchain Development

Verificació formal de les especificacions de la fase 0 d’Ethereum 2.0

Una actualització de ConsenSys R&D en el seu esforç per aportar confiança a la cadena Beacon i als fonaments bàsics d’Eth2. per Franck Cassez, 10 d’agost de 2020 Publicat el 10 d’agost de 2020

L’equip de verificació automatitzada de ConsenSys R&D fa uns mesos que treballem en una especificació i verificació formal de la cadena Beacon. Ens complau informar que s’ha avançat molt i, encara que encara no s’ha completat, hem aconseguit desenvolupar-lo un nucli sòlid i formalment verificat de la cadena Beacon. Per primera vegada, el nostre treball proporciona un nivell de fiabilitat inigualable als fonaments bàsics de la infraestructura Eth2.0.

Metodologia

Verificació vs. proves

Hem utilitzat el premiada llenguatge de programació conscient de la verificació Dafny escriure un formal (funcional i lògic) especificació de cada funció Beacon Chain, un implementació de cada funció, i a prova que la implementació s’ajusta a la seva especificació. En altres paraules, hem comprovat matemàticament l’absència d’errors. Les implementacions que finalment hem demostrat que són correctes es basen les especificacions oficials d’Eth2.0 amb l’advertència que hem corregit i informat d’alguns errors i incoherències.

La nostra metodologia és diferent a la prova que nosaltres demostrar matemàticament conformitat de les funcions a les seves especificacions, per tot entrades. Les proves no poden abastar infinites entrades i, en conseqüència, poden descobrir errors però no demostrar l’absència d’errors.

I el millor és que no necessitem publicar un document ni revisar les proves. Les proves formen part de la base de codi i s’escriuen com a programes. Sí, a Dafny podeu escriure una prova com a programa adequat per a desenvolupadors. També, el les proves es comproven mecànicament per un demostrador del teorema, que no deixa espai per a proves incompletes o defectuoses.

Propietats que hem demostrat

Les propietats van des de l’absència de sota / desbordaments aritmètics i índex fora dels límits, la conformitat de cada funció a les pre / post condicions lògiques (lògica de primer ordre) (exemple merkelise aquí), a altres de més complexes que impliquen composicions de funcions. Per exemple, tenim el següent propietat de la SSZ Serialitzar / Deserialitzar funcions: per a cada objecte x, Deserialise (Serialise (x)) = x, és a dir, deserialitzar un objecte serialitzat retorna l’objecte original. També hem establert un nombre d’invariants, i els va utilitzar per demostrar que les operacions bàsiques de Beacon Chain i ForkChoice (transició_estat, sobre_bloc) en realitat construeix una cadena de blocs: per a qualsevol bloc b del magatzem, els avantpassats de b formen una seqüència finita totalment ordenada que condueix al bloc de gènesi, que és la propietat principal d’una cadena de blocs!

Els avantatges de la verificació formal

Qualsevol metodista formal insisteix que la verificació és una bona pràctica de seguretat. Així és exactament com aquesta metodologia garanteix una infraestructura segura i fiable per a Ethereum 2.0.

Especificació funcional

En primer lloc, hem elevat les especificacions oficials d’Eth2.0 a especificació lògica i funcional formal. Per a cada funció, definim formalment què s’espera que calculi la funció, no com. Això proporciona Especificacions de referència adequades per al desenvolupador agnòstic del llenguatge que es pot utilitzar per desenvolupar implementacions més segures, amb menys esforç.

Modularitat

En segon lloc, les nostres especificacions, implementacions i arquitectura de prova són modular. Com a resultat, podem fer-ho fàcilment experimentar amb noves implementacions (per exemple, optimitzacions) i comprovar el seu impacte en el sistema general. Penseu en un hack intel·ligent per implementar una funció? Canvieu la implementació i demaneu a Dafny que comprovi que encara compleix la seva especificació. Si ho fa, les proves dels components que utilitzen aquesta funció no es veuran afectades.

Executabilitat

En tercer lloc, les nostres implementacions són executable. Podem compilar i executar un programa Dafny. Encara millor, pots automàticament generar codi en alguns llenguatges de programació populars com C #, Go (i aviat Java) des del codi Dafny. Es pot utilitzar per complementar bases de codi existents o per generar proves certificades. La implementació que es vol provar pot utilitzar les nostres funcions demostrades que són correctes per calcular el resultat esperat d’una prova i contrastar-lo amb el seu propi resultat.

Tot en un sol idioma

Per últim, però no menys important, la nostra base de codi és autònom. Conté les especificacions, implementacions, documentacions i proves, tot en un llenguatge de programació únic, llegible, senzill i semànticament ben definit..

Preguntes i consideracions

Què passa amb la solidesa del motor de verificació?

Us preguntareu: “i si el compilador / verificador de Dafny és erroni?” De fet, sabem que Dafny és un buggy (problemes de reposició de dafny), però no confiem en l’absència d’errors a Dafny. Confiem en que Dafny (i el seu motor de verificació) ho sigui so. La solidesa vol dir que quan Dafny informa que les proves són correctes, en efecte són correctes.

Què passa si l’especificació que hem escrit no és l’adequada?

En aquest cas, demostraríem la conformitat amb un requisit incorrecte. Sí, això pot passar i no hi ha cap bala de plata per solucionar aquest problema. No obstant això, com hem esmentat abans, Dafny és executable. Això ens permet executar el codi i tenir certa confiança que les nostres especificacions són les adequades. I les nostres especificacions estan escrites en una lògica de primer ordre sense cap dubte sobre el significat, de manera que si observeu un problema, feu-nos-ho saber i ho solucionarem..

Què passa si Dafny no pot demostrar que una implementació s’ajusta a una especificació?

Això pot passar, però en aquest cas Dafny disposa d’alguns mecanismes de retroalimentació per ajudar a investigar quins passos d’una prova no es poden verificar. I fins ara, sempre hem aconseguit crear proves que Dafny pugui comprovar automàticament.

Agraïm els vostres comentaris, així que consulteu-ho el nostre repositori eth2.0-dafny. Ens ha emocionat veure el desenvolupament d’Ethereum 2.0 assolir les fites recents de testnet i esperem treballar amb equips de l’ecosistema per assegurar-nos que la següent fase de la xarxa es construeix sobre una base sòlida.

Agraïment: gràcies als meus companys d’equip Joanne Fuller, Roberto Saltini (equip de verificació automàtica), Nicolas Liochon i a Avery Erwin pels comentaris sobre una versió preliminar d’aquest post.

Mantingueu-vos al dia amb Ethereum 2.0

Subscriviu-vos al butlletí de notícies ConsenSys per obtenir les darreres notícies d’Eth2 directament a la vostra safata d’entrada. Subscriu-te Ethereum 2.0 Recerca i desenvolupament Seguretat Butlletí Subscriu-te al nostre butlletí per obtenir les últimes novetats, solucions empresarials, recursos per a desenvolupadors i molt més sobre Ethereum. Adreça electrònica Contingut exclusiuSeminari web