Input Output demonstriert Blaster für die Verifizierung von Cardano Smart Contracts

Cardano Community hat eine Präsentation von Blaster veröffentlicht, einem automatisierten Verifizierungswerkzeug, das prüfen soll, ob Cardano Smart Contracts festgelegten Regeln folgen. Die Input Output Ingenieure Romain Soulat und Jean-Frédéric Etienne demonstrieren, wie das Werkzeug diese Eigenschaften untersucht und ein Gegenbeispiel erzeugen kann, wenn es einen Verstoß findet. Sie sprechen außerdem über laufende Arbeiten zur Beweisrekonstruktion und darüber, wie sich Ergebnisse leichter prüfen lassen.

Festlegen, was ein Cardano Smart Contract leisten muss

Smart Contracts legen Bedingungen für Blockchain Transaktionen fest und bestimmen, wie Anwendungen Vermögenswerte handhaben. Ein Entwickler kann zum Beispiel festlegen, dass nur ein autorisierter Nutzer Mittel freigeben darf, die von einem Vertrag gehalten werden. Formale Verifizierung nutzt mathematische Methoden, um zu prüfen, ob ein System Eigenschaften erfüllt, die in einer Spezifikation festgehalten sind. Während ein herkömmlicher Test ausgewählte Fälle untersucht, zielt die formale Verifizierung darauf ab festzustellen, ob eine formulierte Eigenschaft in allen vom Modell abgedeckten Fällen gilt.

Soulat, technischer Leiter für Cardano High Assurance, erklärte, dass Blaster einen großen Teil der Beweisarbeit automatisieren soll. Entwickler müssen weiterhin das Verhalten definieren, das sie prüfen wollen, und die entsprechende Spezifikation bereitstellen. Wenn das Werkzeug einen Verstoß findet, kann es ein Gegenbeispiel zur Prüfung erzeugen. Soulat beschrieb eine Transaktion oder eine Abfolge von Transaktionen, die zeigen könnte, wie jemand anderes als der autorisierte Nutzer eine Ausgabe freischaltet.

Wie Blaster Vertragseigenschaften prüft

Blaster verwendet Lean 4, ein System zum Formulieren mathematischer Aussagen und zum Arbeiten mit Beweisen, zusammen mit einem automatisierten Solver. Zunächst vereinfacht es das Problem; wird die Eigenschaft in dieser Phase nicht entschieden, kann das verbleibende Problem an den Solver übergeben werden. Damit die Prüfungen für Cardano relevant sind, hat das Team Teile der Umgebung formalisiert, in der Verträge laufen, einschließlich Skriptausführung und Transaktionsregeln.

Etienne, Senior Ingenieur für formale Methoden, skizzierte drei mögliche Ergebnisse: Eine Eigenschaft kann als gültig, widerlegt oder unbestimmt gemeldet werden. Ein mit einem widerlegten Ergebnis verknüpftes Gegenbeispiel kann Entwicklern helfen, einen Vertragsfehler, eine fehlende Annahme oder einen Fehler in der Spezifikation zu identifizieren. Ein unbestimmtes Ergebnis bedeutet, dass der Solver nicht festgestellt hat, ob die Eigenschaft gilt. Der Umfang einer Prüfung hängt von den Eigenschaften ab, die die Entwickler formulieren.

[NEWSBREAK]

Beweisrekonstruktion ist in Entwicklung

Entwickler können Verträge, die in Sprachen wie Plinth, Aiken oder Plutarch geschrieben sind, in Untyped Plutus Core kompilieren, die Darstellung, die zur Ausführung von Cardano Skripten verwendet wird. Anschließend können sie den kompilierten Code in Lean 4 importieren und die zu prüfenden Eigenschaften spezifizieren. Input Output hat zuvor zwei Open Source Bibliotheken veröffentlicht, die die für Cardano spezifischen Modelle für diesen Prozess bereitstellen. In einer früheren Demonstration nutzte das Team die Pipeline an einem Beispielvertrag aus einer Sicherheitsherausforderung und erzeugte einen Transaktionskontext, der zeigte, wie der Vertrag ausgenutzt werden konnte.

Etienne erklärte, dass die Beweisrekonstruktion noch in Entwicklung ist. Ziel ist es, Lean die unabhängige Prüfung von Belegen zu einem gültigen Ergebnis zu ermöglichen; das aktuelle Werkzeug erzeugt noch keinen rekonstruierten Lean Beweis, wenn der Solver dieses Ergebnis liefert. Soulat skizzierte außerdem Pläne für klarere Ansichten der Gegenbeispiele, sodass Entwickler die Transaktionsdetails hinter einer fehlgeschlagenen Eigenschaft prüfen können.