Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

Bezpieczeństwo · Edukacja · Analityka · Weryfikacja formalna · Wykonywanie symboliczne · Narzędzia do debugowania · Weryfikacja w czasie wykonywania · Vyper

Społeczności runtimeverification/evm-semantics(586 ☆)

KEVM to wykonywalna semantyka EVM w K-framework: wskaż jej kod bajtowy, gdy potrzebujesz wykonania ze sprawdzeniem zgodności, eksploracji symbolicznej, wnioskowania o gazie lub dowodów, które ściśle śledzą zasady Ethereum.

Related resources

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol podnosi testy właściwości Foundry do dowodów opartych na KEVM, dzięki czemu możesz dążyć do formalnych gwarancji przy mniejszej ilości ręcznie pisanej specyfikacji niż w przypadku samego KEVM.

hax

hax to narzędzie do tłumaczeń o wysokiej pewności (high assurance) dużego podzbioru języka Rust na języki formalne, takie jak F* lub Rocq.

Act

Act to deklaratywny język specyfikacji i zestaw narzędzi Ethereum do opisywania wszystkich zachowań programu EVM, dzięki czemu solvery SMT, systemy dowodzenia twierdzeń lub narzędzia analizy ekonomicznej mogą wnioskować o poprawności na poziomie kodu bajtowego i kompatybilności zachęt, w tym o automatycznych dowodach udoskonalenia w stosunku do konkretnych implementacji.

Verifereum

Verifereum łączy inteligentne kontrakty Ethereum z dowodzeniem twierdzeń opartym na HOL4, dzięki czemu możesz dążyć do bardzo silnych gwarancji poprawności, gdy zautomatyzowane podejścia SMT nie wystarczają.