Kurz erklärt: Mythril ist ein quelloffenes Sicherheitsanalyse-Werkzeug für Ethereum-Smart-Contracts. Es untersucht EVM-Bytecode mittels symbolischer Ausführung und SMT-Solving, um Schwachstellen automatisiert aufzudecken.
Herkunft
Mythril wurde ab etwa 2017 entwickelt und ist eng mit dem Umfeld von ConsenSys verbunden. Es bildete eine Grundlage für den späteren kommerziellen Analysedienst MythX. Das Werkzeug ist in Python geschrieben und quelloffen verfügbar.
Im Unterschied zu rein statischen Werkzeugen wie Slither arbeitet Mythril auf der Ebene des kompilierten EVM-Bytecodes und muss daher nicht zwingend den Solidity-Quellcode kennen.
Funktionsweise
Mythril verwendet symbolische Ausführung: Statt konkreter Werte werden Eingaben als symbolische Variablen behandelt und mögliche Programmpfade systematisch durchlaufen. Ein SMT-Solver (typischerweise Z3) prüft dabei, ob Bedingungen erfüllbar sind, die zu einem Fehlerzustand führen.
- Analyse der Ethereum Virtual Machine (EVM) auf Bytecode-Ebene;
- Erkennung von Mustern wie Integer-Überläufen, unsicheren Aufrufen oder unautorisierten Zugriffen;
- Kombinierbarkeit mit anderen Werkzeugen über die Kommandozeile und eine API.
Symbolische Ausführung kann tiefer liegende Pfade erreichen als einfache statische Analyse, ist jedoch rechenintensiver und kann bei sehr komplexen Contracts an Grenzen stoßen (Pfadexplosion).
Einordnung im Prüfprozess
Mythril wird häufig gemeinsam mit statischer Analyse und Fuzzing eingesetzt, um verschiedene Klassen von Schwachstellen abzudecken. In Sicherheitsaudits und bei Wettbewerbsplattformen wie Code4rena sowie Bug-Bounty-Programmen über Immunefi gehört es zum verbreiteten Werkzeugkasten der Prüfer.
Häufige Fragen
Was macht Mythril?
Mythril analysiert EVM-Bytecode von Ethereum-Smart-Contracts mittels symbolischer Ausführung und meldet mögliche Schwachstellen wie unsichere Aufrufe oder Zugriffsfehler.
Was ist symbolische Ausführung?
Bei der symbolischen Ausführung werden Eingaben als symbolische Variablen statt konkreter Werte behandelt. Ein SMT-Solver prüft, ob es Eingaben gibt, die zu einem fehlerhaften Zustand führen.
Worin unterscheidet sich Mythril von Slither?
Slither führt eine statische Analyse auf Quellcode-Ebene durch, während Mythril auf Bytecode-Ebene arbeitet und mittels symbolischer Ausführung Programmpfade durchläuft. Beide ergänzen sich.
Was ist der Zusammenhang zu MythX?
Mythril bildete eine Grundlage für den kommerziellen Analysedienst MythX aus dem ConsenSys-Umfeld. Mythril selbst ist quelloffen und frei nutzbar.
Hat symbolische Ausführung Grenzen?
Ja. Bei sehr komplexen Contracts kann die Zahl der Programmpfade stark ansteigen (Pfadexplosion), was die Analyse rechenintensiv macht und nicht immer alle Pfade abdeckt.
Zusammenfassung
Mythril ist ein quelloffenes Sicherheitswerkzeug für Ethereum-Smart-Contracts, das EVM-Bytecode mittels symbolischer Ausführung und SMT-Solving analysiert. Es entstand im Umfeld von ConsenSys, bildete eine Grundlage für MythX und wird in Audits gemeinsam mit statischer Analyse und Fuzzing eingesetzt.
Weiterführende Quellen
- Mythril auf GitHub (Consensys): github.com