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.
Sascha Pleßberger (Sun,) studied this question.