Semantic Verification of Ethereum Smart Contracts using KEVM

Abstract

Ethereum-Smart Contracts verwalten häufig erhebliche finanzielle Werte. Da sie praktisch unveränderlich sind und häufig böswilligen Akteuren ausgesetzt sind, die durch finanziellen Gewinn motiviert sind, stellt die semantische Korrektheit eine zentrale Sicherheitsanforderung dar. Etablierte Testmethoden reichen oft nicht aus, um die Korrektheit über alle möglichen Ausführungspfade hinweg zu gewährleisten. Daher stellt die formale Verifikation ein wesentliches Mittel dar, um solche Sicherheitsgarantien zu stärken. Diese Arbeit untersucht die auf symbolischer Ausführung basierende Verifikation von Ethereum-Smart-Contracts unter Verwendung des KEVM-Frameworks sowie zweier darauf aufbauender Werkzeuge auf höherer Abstraktionsebene: ACT und Kontrol. Diese Arbeit behandelt Fragestellungen hinsichtlich der Ausdrucksstärke und Konstruktion von Beweisen sowie der Nutzbarkeit und Interpretierbarkeit sowohl von Beweisdefinitionen als auch von generierten Beweisartefakten. Es wird untersucht, ob und welche praktischen Herausforderungen bei der Verwendung von KEVM und zugehörigen Werkzeugen auftreten, einschließlich der Syntax, der verfügbaren Debugging-Werkzeuge sowie der Analyse von Beweisen und Gegenbeweisen. Anschließend erfolgt eine Evaluierung, wie semantische Eigenschaften über alle Werkzeuge hinweg spezifiziert werden können und wie präzise diese spezifiziert werden, wobei insbesondere die Zielkonflikte zwischen unterschiedlichen Abstraktionsebenen hervorgehoben werden. Darüber hinaus verifizieren wir semantische Eigenschaften von ERC20-Token-Smart-Contracts mit besonderem Fokus darauf, ob bestimmte Einträge in der Common Vulnerabilities and Exposures (CVE)-Datenbank tatsächlich korrekt sind oder mithilfe von KEVM widerlegt werden können. Zu diesem Zweck analysieren wir die gemeldete Schwachstelle, formulieren ein formales Argument gegen die behauptete Verletzung und konstruieren darauf aufbauend einen Beweis unter Verwendung von Kontrol. Dabei zeigen wir, wie semantische Eigenschaften innerhalb des Frameworks formuliert und verifiziert werden können. Abschließend untersuchen wir die Community-Aktivität rund um KEVM und dessen Ökosystem. Dazu werden GitHub-Repository-Metriken sowie Kommunikationsdaten aus Discord ausgewertet, um Entwicklungsaktivität, Dynamiken der Beitragenden sowie Muster im Nutzer-Support zu analysieren. Diese kombinierte Perspektive aus technischer und empirischer Sicht liefert eine ganzheitliche Betrachtung von KEVM sowohl als formales Verifikationsframework als auch als Entwickler-Ökosystem.

Ethereum smart contracts often hold a significant amount of funds. Since they are virtually immutable and are often exposed to malicious agents incentivised by monetary gain, semantic correctness is a critical security concern. Established testing techniques are often insufficient to guarantee correctness across all possible execution paths. As such, formal verification is an essential tool in strengthening such security guarantees. This thesis investigates symbolic-execution-based verification of Ethereum smart contracts using the KEVM framework and two higher-level tools built on top of it: ACT and Kontrol. Our work considers questions regarding proof expressiveness and construction, usability and understandability of both proof definitions and generated proof artefacts. We will examine if and what practical challenges occur during the use of KEVM and its related tools, including syntax, available debuggers and proof or refutation analysis. Next, an evaluation is done on how semantic properties can be specified across all tools and how accurate they are, highlighting the trade-offs between abstraction levels. Furthermore, we verify semantic properties of ERC20 token contracts, with a focus on determining whether certain reports in the Common Vulnerabilities and Exposures (CVE) database are indeed correct or can be refuted using KEVM. To that end, we examine the vulnerability reported, give a formal argument against the reported violation and from there construct a proof using Kontrol. Using this approach, we demonstrate how semantic properties can be expressed and verified within the framework. Finally, we analyse community activity around KEVM and its ecosystem. GitHub repository metrics and Discord communication data are evaluated to assess development activity, contributor dynamics, and user support patterns. This combined technical and empirical perspective provides a comprehensive view of KEVM as both the formal verification framework and the developer ecosystem.