Formalna weryfikacja specyfikacji Ethereum 2.0 fazy 0

blog 1AktualnościDevelopersEnterpriseBlockchain ExplainedWydarzenia i konferencjePrasaBiuletyny

Zapisz się do naszego newslettera.

Adres e-mail

Szanujemy twoją prywatność

HomeBlogBlockchain Development

Formalna weryfikacja specyfikacji Ethereum 2.0 fazy 0

Aktualizacja od ConsenSys R&D o ich wysiłkach na rzecz zapewnienia wiarygodności Beacon Chain i podstawowym fundamentom Eth2. autor: Franck Cassez 10 sierpnia 2020 opublikowany 10 sierpnia 2020

dafny weryfikuje bohatera bloga

Zespół automatycznej weryfikacji w ConsenSys R&D od kilku miesięcy pracuje nad formalną specyfikacją i weryfikacją Beacon Chain. Z radością informujemy, że osiągnięto duży postęp i chociaż jeszcze nie ukończono, udało nam się rozwinąć solidne i formalnie zweryfikowane jądro Beacon Chain. Po raz pierwszy nasza praca zapewnia niezrównany poziom zaufania do podstawowych fundamentów infrastruktury Eth2.0.

Metodologia

Weryfikacja a testowanie

Użyliśmy wielokrotnie nagradzany język programowania obsługujący weryfikację Dafny napisać formalny (funkcjonalne i logiczne) specyfikacja każdej funkcji Beacon Chain, plik realizacja każdej funkcji oraz a dowód że implementacja jest zgodna ze specyfikacją. Innymi słowy, zweryfikowaliśmy matematycznie brak błędów. Implementacje, które ostatecznie okazały się poprawne, są oparte na oficjalne specyfikacje Eth2.0 z zastrzeżeniem, że naprawiliśmy i zgłosiliśmy kilka błędów i niespójności.

Nasza metodologia różni się od testowania, tak jak my matematycznie udowodnić zgodność funkcji z ich specyfikacjami, np wszystko wejścia. Testowanie nie może obejmować nieskończenie wielu danych wejściowych, w wyniku czego można wykryć błędy, ale nie udowodnić ich braku.

A najlepsze jest to, że nie musimy publikować artykułu ani recenzować dowodów. Dowody są częścią kodu źródłowego i są napisane jako programy. Tak, w Dafny możesz napisać dowód jako program przyjazny dla programistów. Ponadto dowody są sprawdzane mechanicznie przez twierdzenie twierdzące, nie pozostawiając miejsca na niekompletne lub wadliwe dowody.

Właściwości, które udowodniliśmy 

Właściwości wahają się od braku arytmetyczne pod / przepełnienia i indeks poza granicami, zgodność każdej funkcji z logicznymi (logiką pierwszego rzędu) warunkami wstępnymi / końcowymi (przykład merkelise tutaj), do bardziej złożonych, obejmujących kompozycje funkcji. Na przykład mamy następujące własność SSZ Serialise / Deserialise funkcje: dla każdego obiektu x Deserialise (Serialise (x)) = x, tj. deserializacja zserializowanego obiektu zwraca oryginalny obiekt. Stworzyliśmy również liczba niezmienników, i użył ich do udowodnienia, że ​​podstawowe operacje Beacon Chain i ForkChoice (state_transition, on_block) tak właściwie zbuduj łańcuch bloków: dla dowolnego bloku b w sklepie przodkowie b tworzą skończoną, całkowicie uporządkowaną sekwencję prowadzącą do bloku genezy, który jest główną właściwością łańcucha bloków!

Korzyści z weryfikacji formalnej

Każdy formalny metodolog upierałby się, że weryfikacja jest najlepszą praktyką w zakresie bezpieczeństwa. Oto dokładnie, w jaki sposób ta metodologia zapewnia bezpieczną i godną zaufania infrastrukturę dla Ethereum 2.0.


Specyfikacja funkcjonalna

Po pierwsze, podnieśliśmy oficjalne specyfikacje Eth2.0 do formalna specyfikacja logiczna i funkcjonalna. Dla każdej funkcji formalnie definiujemy co funkcja ma obliczyć, nie jak. To zapewnia Specyfikacje referencyjne przyjazne dla programistów, niezależne od języka które można wykorzystać do opracowania bezpieczniejszych implementacji przy mniejszym wysiłku. 

Modułowość

Po drugie, nasze specyfikacje, implementacje i architektura dowodu są modułowy. Dzięki temu możemy łatwo eksperymentuj z nowymi implementacjami (np. optymalizacjami) i sprawdź ich wpływ na cały system. Pomyśl o sprytnym sposobie zaimplementowania funkcji? Zmień implementację i poproś firmę Dafny o sprawdzenie, czy nadal jest zgodna ze specyfikacją. Jeśli tak, nie ma to wpływu na dowody komponentów korzystających z tej funkcji.

Wykonalność

Po trzecie, nasze wdrożenia są wykonywalny. Możemy skompilować i uruchomić program Dafny. Nawet lepiej, możesz automatycznie wygeneruj kod w niektórych popularnych językach programowania, takich jak C #, Go (i wkrótce Java) z kodu Dafny. Można to wykorzystać do uzupełnienia istniejących baz kodu lub do generowania certyfikowane testy. Testowana implementacja może korzystać z naszych sprawdzonych i poprawnych funkcji, aby obliczyć oczekiwany wynik testu i porównać go z własnym wynikiem.   

Wszystko w jednym języku

Wreszcie, nasza baza kodu to samowystarczalny. Zawiera specyfikacje, implementacje, dokumentacje i dowody w jednym, czytelnym, prostym i dobrze zdefiniowanym semantycznie języku programowania.

Pytania i uwagi 

A co z solidnością silnika weryfikacyjnego?

Możesz się zastanawiać, „a co jeśli kompilator / weryfikator Dafny zawiera błędy?” Właściwie wiemy, że Dafny jest buggy (problemy z repozytorium dafny), ale nie polegamy na braku błędów w Dafny. Polegamy na Dafny (i jego silniku weryfikacyjnym) dźwięk. Trafność oznacza, że ​​kiedy Dafny zgłasza, że ​​dowody są poprawne, są one rzeczywiście poprawne. 

A co, jeśli napisana przez nas specyfikacja nie jest właściwa? 

W takim przypadku udowodnilibyśmy zgodność z niewłaściwym wymaganiem. Tak, może się to zdarzyć i nie ma srebrnej kuli, która rozwiązałaby ten problem. Jednak, jak wspomnieliśmy wcześniej, Dafny jest wykonywalny. Dzięki temu możemy uruchomić kod i uzyskać pewność, że nasze specyfikacje są właściwe. A nasze specyfikacje są napisane w logice pierwszego rzędu, bez miejsca na spór o znaczenie, więc jeśli zauważysz problem, daj nam znać, a my go naprawimy.

Co jeśli Dafny nie może udowodnić, że implementacja jest zgodna ze specyfikacją? 

Może się to zdarzyć, ale w tym przypadku Dafny ma pewne mechanizmy zwrotne, które pomagają zbadać, jakich kroków dowodu nie można zweryfikować. Do tej pory zawsze udawało nam się budować dowody, które Dafny może automatycznie sprawdzić.

Czekamy na Twoją opinię, więc sprawdź nasze repozytorium eth2.0-dafny. Cieszymy się, że rozwój Ethereum 2.0 osiąga ostatnie kamienie milowe w sieci testowej i nie możemy się doczekać współpracy z zespołami w całym ekosystemie, aby upewnić się, że kolejna faza sieci jest zbudowana na solidnych fundamentach.

Podziękowania: Dziękuję moim kolegom z zespołu Joanne Fuller, Roberto Saltini (zespół automatycznej weryfikacji), Nicolasowi Liochonowi i Avery Erwin za komentarze do wstępnej wersji tego posta.

Bądź na bieżąco z Ethereum 2.0

Zapisz się do newslettera ConsenSys, aby otrzymywać najnowsze wiadomości o Eth2 prosto do swojej skrzynki odbiorczej. Badania i rozwój Ethereum 2.0BezpieczeństwoNewsletterZapisz się do naszego newslettera, aby otrzymywać najnowsze wiadomości o Ethereum, rozwiązania dla przedsiębiorstw, zasoby dla programistów i nie tylko.Jak zbudować udany produkt BlockchainWebinar

Jak zbudować udany produkt Blockchain

Jak skonfigurować i uruchomić węzeł EthereumWebinar

Jak skonfigurować i uruchomić węzeł Ethereum

Jak zbudować własny interfejs API EthereumWebinar

Jak zbudować własny interfejs API Ethereum

Jak stworzyć token społecznościowyWebinar

Jak stworzyć token społecznościowy

Korzystanie z narzędzi bezpieczeństwa w tworzeniu inteligentnych kontraktówWebinar

Korzystanie z narzędzi bezpieczeństwa w tworzeniu inteligentnych kontraktów

Przyszłość finansów, aktywów cyfrowych i DeFiWebinar

Przyszłość finansów: aktywa cyfrowe i DeFi

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me
Like this post? Please share to your friends:
Adblock
detector
map