Sicherheit, Tests & Formale Verifikation

Wir sind Runtime Verification, ein Forschungs- und Entwicklungsunternehmen, das rigorose Tools entwickelt, um die Sicherheit und Korrektheit kritischer Systeme zu gewährleisten. Unser Team hat KEVM entwickelt, die vollständigste und praxiserprobteste formale Semantik der Ethereum Virtual Machine (EVM), geschrieben im K Framework. KEVM ist nicht nur eine Spezifikation, es ist eine ausführbare Spezifikation, die verwendet werden kann, um symbolisch über Smart Contracts nachzudenken, Konformitätstests durchzuführen, den Gasverbrauch zu analysieren, Programme zu debuggen und Korrektheitseigenschaften formal zu verifizieren. Es besteht die vollständige Ethereum-Testsuite und wird verwendet, um hochwertige Verträge zu verifizieren, einschließlich ERC-20-Token in sowohl Solidity als auch Vyper. Wir haben kürzlich die Semantik aktualisiert, um das Pectra-Upgrade zu unterstützen. KEVM wird aktiv von Kontrol genutzt – unserem formalen Verifizierungstool für Solidity, das von führenden Teams im EVM-Ökosystem aktiv genutzt wird, einschließlich Optimism, Ethereum Foundation, Lido, Uniswap, sowie von Sicherheitsforschern und Auditoren in der breiteren Ethereum-Community. Wir pflegen dieses Repository aktiv, tragen zur Protokollevolution von Ethereum bei und integrieren uns in Entwicklertools wie Foundry. Durch KEVM verschieben wir die Grenzen dessen, was in nachweislich korrekter und sicherer Smart-Contract-Infrastruktur möglich ist.

Act ist eine Spezifikationssprache für Smart Contracts und ein Toolkit für die formale Verifikation. Act-Spezifikationen sind eine formale, abstrakte Beschreibung aller möglichen Verhaltensweisen eines EVM-Programms. Act ermöglicht die Nutzung vieler bestehender Allzweck-Verifikationstools, um Eigenschaften der Spezifikation zu beweisen. Zu diesen Tools gehören SMT-Solver (cvc5, z3, bitwuzla), Theorembeweiser (Coq) und Tools für ökonomische Analysen (CheckMate, Open Games). Act-Spezifikationen können automatisch als äquivalent zu konkreten Implementierungen in der EVM bewiesen werden. Für sehr einfache Verträge können Act-Spezifikationen automatisch aus EVM-Bytecode generiert werden. Dies ist eine End-to-End-Pipeline, die prinzipienbasiertes Schlussfolgern über High-Level-Eigenschaften von EVM-Bytecode unterstützt. Sie unterstützt das Schlussfolgern sowohl über Korrektheit (z. B. Buchhaltungsinvarianten) als auch über ökonomische Eigenschaften (z. B. Anreizkompatibilität). Act-Spezifikationen dienen als High-Level-Darstellung von Smart Contracts und ermöglichen eine einfache Integration bestehender Allzweck-Analyse- und Verifikationstools in den EVM-Kontext.

Titanoboa ist ein Vyper-Interpreter und Test-Framework, das eine moderne, integrierte Entwicklungserfahrung für Vyper-Smart-Contracts bietet. Es ermöglicht Entwicklern, Vyper-Verträge direkt in Python zu testen und zu debuggen, und bietet Funktionen wie Pretty Tracebacks, Forking, Debugging-Funktionen, Pytest-Integration und Out-of-the-Box-Fuzzing. Über seine eigenständigen Fähigkeiten hinaus dient Titanoboa als Grundlage für andere beliebte Test-Frameworks wie Ape und Moccasin und ist ein zentraler Bestandteil der Infrastruktur für das Vyper-Ökosystem.