Key points are not available for this paper at this time.
In diesem Papier stellen wir ein formales Verifikationswerkzeug für den Ethereum Virtual Machine (EVM) Bytecode vor. Um genau über alle möglichen Verhaltensweisen des EVM Bytecodes nachzudenken, haben wir KEVM, eine vollständige formale Semantik des EVM, übernommen und den Theorembeweiser der Reichbarkeit von K-Framework instanziiert, um einen korrekt-konstruierten deduktiven Verifier für den EVM zu erzeugen. Wir haben den Verifier weiter optimiert, indem wir EVM-spezifische Abstraktionen und Lemmas eingeführt haben, um seine Skalierbarkeit zu verbessern. Unser EVM-Verifier wurde verwendet, um verschiedene hochkarätige Smart Contracts zu verifizieren, einschließlich des ERC20-Tokens, Ethereum Casper und DappHub MakerDAO-Verträge.
Park et al. (Fr,) haben diese Frage untersucht.