Eliminieren Sie intelligente Vertragsfehler mit TLA+

Im Juni 2016 herrschte große Aufregung darüber, dass „The DAO“, basierend auf der Ethereum-Blockchain, im Begriff war, der weltweit erste vollständig digitale, dezentrale Investmentfonds zu werden.
Doch innerhalb weniger Wochen wurde es zum Aushängeschild für DeFi-Hacks, nachdem Angreifer Ether im Wert von 50 Millionen US-Dollar von ihm gestohlen hatten.
Um das DAO zu knacken, nutzte der Angreifer eine sogenannte Reentrancy-Schwachstelle aus, eine Schwachstelle in der Parallelität, bei der eine Methode eines bestimmten Smart Contracts aufgerufen wird, während eine andere Methode noch ausgeführt wird, und das DAO ist nur ein Teil der langfristigen Entwicklung des DAO Der erste intelligente Vertrag weist solche Fehler auf.
Prominente Nachfolger sind Uniswap/Lendf.Me, dem im Jahr 2020 25 Millionen US-Dollar gestohlen wurden, CREAM, dem im Jahr 2021 18 Millionen US-Dollar gestohlen wurden, und Fei, dem im Jahr 2022 80 Millionen US-Dollar gestohlen wurden.
Der Grund dafür, dass diese Fehler bestehen bleiben, besteht darin, dass es zu unerwarteten Code-Interaktionen kommen kann, die über den gesamten Smart Contract verstreut sind, manchmal sogar in verschiedenen Smart Contracts. Die Anzahl solcher Code-Interaktionen kann sehr groß sein, was es für Menschen schwierig macht, unbeabsichtigte Smart Contracts zu erkennen und zu beseitigen . Code erforderlich.
Darüber hinaus ist es oft schwierig, diese Interaktionen automatisch und systematisch zu testen.
TLA+: Der Vernichter
Enter Temporal Logic of Actions (TLA+), eine Sprache zur Spezifikation und Validierung komplexer Systeme, findet nicht nur Fehler, sondern überprüft auch deren Existenz.
Wie ist das möglich, fragen Sie? TLA+ verfügt über eine Reihe von Werkzeugen zur einfachen formalen Verifizierung in Form der sogenannten Modellprüfung. Durch Modellprüfung werden alle möglichen gleichzeitigen Interaktionen des Codemodells – genau die Bereiche, die schwer zu testen sind – umfassend untersucht und Fehler gefunden.
Stellen Sie sich einen Kammerjäger vor, der jeden Winkel und jede Ritze ausleuchtet, um unerwünschte Schädlinge, die sich in dunklen Ecken verstecken und oft übersehen oder ignoriert werden, aufzudecken und zu beseitigen. Wichtig ist, dass die Modellprüfung nach der Erstellung des Codemodells fast keine menschliche Eingabe mehr erfordert, was sie äußerst kosteneffektiv macht.
Zur Veranschaulichung einige erfundene Zahlen: Wenn Branchenstandardpraktiken wie Tests und Sicherheitsüberprüfungen 80 % der Fehler beseitigen und eine „schwerwiegende“ formale Verifizierung 99 % beseitigt, eliminiert die Verwendung von TLA+ 90 % mit nur einer kleinen Anzahl aufwändiger Verifizierungsbemühungen.
TLA+ und Internetcomputer
Unser Ingenieurteam verwendet TLA+, um alle Aspekte des Internet-Computings zu analysieren, einschließlich der sicherheitskritischen Smart Contracts, die auf der Plattform ausgeführt werden. Obwohl Ethereum und Internetcomputer unterschiedliche Ausführungsmodelle haben, können in Smart Contracts auf beiden Blockchains Wiedereintrittsfehler auftreten.
Tatsächlich ermöglichen Internetcomputer aufgrund ihres hohen Durchsatzes mehrere gleichzeitige Aufrufe eines einzelnen Smart Contracts, was von den Autoren von Smart Contracts eine größere Sorgfalt erfordert, um unerwünschte gleichzeitige Interaktionen zu verhindern. Da Sicherheit für den Erfolg von Computern im Internet von entscheidender Bedeutung ist, wird TLA+ in vielen Smart Contracts verwendet, um Fehler während der Entwicklungsphase zu erkennen.
Kürzlich wurde ein TLA+-Analysecontainer (intelligente Verträge für Computer im Internet) für den neu veröffentlichten Chain-Key Bitcoin (ckBTC) durchgeführt, dessen Ergebnisse ich im Folgenden mitteilen werde.
ckBTC-Smart-Vertrag
Um über die TLA+-Analyse von ckBTC zu sprechen, beginnen wir mit einem allgemeinen Überblick über ckBTC. ckBTC ist ein Internet-Computer-nativer Token, der im Verhältnis 1:1 sicher durch Bitcoin (BTC) gedeckt ist.
Das ckBTC-Ledger ist ein Container-Smart-Contract auf der Computer-Blockchain des Internets, der verfolgt, wie viel ckBTC jeder Endbenutzer besitzt. Mit demselben Hauptbuch können Endbenutzer ihre ckBTC schneller und kostengünstiger an andere Endbenutzer übertragen als BTC über das Bitcoin-Netzwerk.
Um ckBTC in BTC und zurück umzuwandeln, interagieren Endbenutzer mit einem anderen Smart Contract, dem ckBTC Minter.
Auf einer hohen Ebene sieht der Konvertierungsvorgang von BTC zu ckBTC folgendermaßen aus:
Schritte zum Erhalt von ckBTC:
1. Der Endbenutzer überträgt zunächst einige BTC an eine benutzerspezifische Bitcoin-Einzahlungsadresse. Alle Einzahlungsadressen werden aufgrund der Kettenschlüssel-ECDSA-Signatur vollständig durch den Code des ckBTC-Minter-Smart-Containers gesteuert, wodurch ein neues UTXO erstellt wird, das der Einzahlung gehört Adresse;
2. Der Endbenutzer benachrichtigt den ckBTC Mint Smart Contract über das neu eingezahlte UTXO, indem er die Mint auffordert, das Benutzerguthaben zu aktualisieren;
3. Der Minter-Smart-Vertrag nutzt dann die Bitcoin-Integration von Internetcomputern, um alle UTXOs abzurufen, die der vom Minter kontrollierten, aber benutzerspezifischen Einzahlungsadresse gehören. Der Minter wählt dann neue UTXOs aus dem Bitcoin-Netzwerk aus, indem er ihnen Gegenprüfungen sendet seine interne Buchhaltungsliste der von ihm verarbeiteten UTXOs;
4. Schließlich weist der Minter das Hauptbuch an, neue ckBTC für alle neuen UTXOs im Verhältnis 1:1 zu prägen, und sobald der Vorgang abgeschlossen ist, fügt er die neu entdeckten UTXOs der Liste der verarbeiteten UTXOs hinzu.
Haftungsausschluss: Der oben beschriebene Prozess lässt der Einfachheit halber den KYT-Prozess (Know Your Transaction) weg.
Der ckBTC-Smart-Vertrag erfüllt TLA+
Das oben dargestellte allgemeine Bild verbirgt tatsächlich ein subtiles Parallelitätsproblem, und die gute Nachricht ist, dass wir das Problem mithilfe des TLA+-Toolkits erkennen können.
Doch bevor TLA+ etwas erkennen kann, müssen wir ihm zunächst zwei Dinge zur Verfügung stellen:
Erstellen Sie ein Modell unseres Systems mit der Sprache TLA+
Geben Sie die TLA+-Eigenschaften an, die das System voraussichtlich implementieren soll
Bei diesem Modell handelt es sich um eine vereinfachte, aber dennoch vollständig definierte Version des Systems, das in unserem Fall den Minter-Smart-Vertrag, aber auch alle anderen relevanten Teile des Systems, nämlich den Ledger-Vertrag und das Bitcoin-Netzwerk, umfasst.
Für jede Komponente modellieren wir ihren Status und wie die relevanten Aktionen, die ein Endbenutzer ausführen könnte (z. B. BTC oder ckBTC übertragen, BTC einzahlen oder verschiedene vom Minter bereitgestellte Aktionen aufrufen), den Status ändern.
Alle diese Elemente sind im Modell etwas vereinfacht, wobei Teile, auf die sich die Analyse konzentriert (z. B. der Minter-Code), detaillierter modelliert werden, während andere Teile (z. B. das Bitcoin-Netzwerk) weniger detailliert modelliert werden, tatsächlich ein TLA+-Modell ähnelt einer detaillierten Designspezifikation eines Systems.
Intuitiv besteht die Hauptfunktion, die wir implementieren möchten, darin, sicherzustellen, dass unser ckBTC vollständig unterstützt wird. Mit anderen Worten: Kein Endbenutzer sollte in der Lage sein, seine eingezahlten BTC „doppelt auszugeben“, um mehr ckBTC zu erhalten, als er eingezahlt hat.
Aber um eine solche Eigenschaft zu analysieren, müssen wir diese Intuition sehr präzise machen, indem wir sie formal in der TLA+-Sprache ausdrücken. Unsere formale Definition ist, dass das Gesamtangebot an ckBTC (d. h. die Summe aller ckBTC-Guthaben des Endbenutzers, wie im ckBTC-Ledger gespeichert) die Gesamtmenge an BTC, die vom Münzbehälter kontrolliert wird (d. h. den Wert aller), nicht überschreitet UTXOs, die einer Einzahlungsadresse gehören).
Erkennen und lösen Sie Probleme
Sobald wir das Modell und die Eigenschaften erstellt haben, kann das TLA+-Toolkit das Modell analysieren. Um die Analyse durchzuführen, definieren wir zunächst die Einstellungen für die Ausführung der Analyse. Unser Setup für ckBTC umfasst beispielsweise nur zwei verschiedene Endbenutzer und einen kleinen Teil des gesamten Bitcoin-Angebots (z. B. 5 Satoshis).
Obwohl dieser Rahmen sehr begrenzt ist, zeigen empirische Studien, dass die überwiegende Mehrheit der Probleme in Computersystemen in einer kleinen Anzahl von Einheiten zu finden sind. Der kleine Aufbau ermöglicht es der Analyse, systematisch alle vom Modell definierten möglichen Aktionssequenzen zu untersuchen und zu prüfen, ob die vorgeschriebenen Eigenschaften unter einer solchen Sequenz gelten.
Darüber hinaus läuft die Analyse völlig automatisch ab, erfordert also keine menschliche Eingabe, und wenn diese Eigenschaften nicht zutreffen, liefert sie uns die genaue Abfolge von Vorgängen, die diese Eigenschaft verletzen.
Beispielsweise kann eine Analyse ergeben, dass wir in einem Szenario wie dem unten abgebildeten gegen unsere Eigenschaft „Kein ungesichertes ckBTC“ verstoßen können:
Hier:
Endbenutzer zahlen wie zuvor BTC ein;
Nun weist der Endbenutzer den ckBTC-Minter jedoch an, den Kontostand zweimal schnell hintereinander zu aktualisieren, und auf einem Internetcomputer können diese Aktualisierungen gleichzeitig mit anderen Smart Contracts interagiert werden;
Zwei gleichzeitig laufende Updates fragen das Bitcoin-Netzwerk nach allen vom Endbenutzer hinterlegten UTXOs, und beide erhalten als Antwort dasselbe UTXO, das in Schritt 1 hinterlegt wurde. Da sich das UTXO noch nicht in der „verarbeiteten“ Liste befindet, denken beide Updates, dass UTXO neu ist;
Beide Aktualisierungen weisen das Hauptbuch an, in Schritt 4 die entsprechende Menge an ckBTC zu prägen.
Daher befinden wir uns am Ende von Schritt 4 in einem Zustand, in dem der ckBTC-Vorrat doppelt so hoch ist wie die Summe der UTXOs in Einzahlungsadressen, was gegen unsere Eigenschaft „kein nicht unterstütztes ckBTC“ verstößt.
Beachten Sie, dass dieser Fehler nur auftritt, weil Aktualisierungen des Endbenutzer-Guthabens gleichzeitig ausgeführt werden – es handelt sich tatsächlich um einen wiederkehrenden Fehler im gleichen Stil wie der, der The DAO zum Absturz gebracht hat.
Eine Möglichkeit, dieses Problem zu lösen, besteht darin, zu verhindern, dass Saldenaktualisierungen für denselben Endbenutzer parallel ausgeführt werden. Dies können wir erreichen, indem wir den Minter den Endbenutzer beim Start der Saldenaktualisierung in einer „gesperrten“ Benutzerliste speichern und dort aufbewahren lassen für die Dauer der Update-Liste, um dies zu erreichen.
Wenn der Endbenutzer versucht, eine weitere gleichzeitige Aktualisierung des Kontostands zu initiieren, prüft die Aktualisierung zunächst diesen bestimmten Endbenutzer, findet ihn in der Liste der gesperrten Benutzer und bricht dann ab.
Beachten Sie, dass wir den Angriff hier etwas vereinfachen: Das Sperren ist tatsächlich ein recht verbreitetes Muster für IC-Smart-Contracts, und ckBTC-Minter haben es von Anfang an eingesetzt. Eine unsachgemäß durchgeführte Sperrung öffnet jedoch Tür und Tor für die oben genannten Angriffe, die TLA+ erkennen kann.
Darüber hinaus haben wir einige Randfälle gefunden, die gegen „kein nicht unterstütztes ckBTC“ und andere wichtige Eigenschaften verstießen, und nachdem wir alle Korrekturen angewendet hatten, konnte TLA+ überprüfen und bestätigen, dass es in unserem definierten Setup keine weiteren Eigenschaftsverstöße gab.
Sollten Sie TLA+ für Ihre Smart Contracts verwenden?
Absolut! Okay, okay, vielleicht sollte ich eine differenziertere Antwort geben, die unser Forschungs- und Entwicklungsteam für kritische Smart Contracts auf Internetcomputern verwendet, wenn es um nicht triviale Parallelität geht.
Beispielsweise deckte die TLA+-Analyse subtile Parallelitätsfehler in den Internet Computer Governance- und Ledger-Containern auf, die bei früheren manuellen Sicherheitsüberprüfungen übersehen wurden und zu erheblichen Problemen, Fällen und Punkten hätten führen können – TLA+ war maßgeblich an der Aufdeckung solch heikler Probleme beteiligt. Ein absoluter Knaller.
Natürlich ist für den Erwerb des Know-hows und den anschließenden Aufbau des Modells ein Preis zu zahlen, aber empirisch gesehen ist der Preis angemessen, insbesondere angesichts der hohen Risiken der Blockchain-Sicherheit.
Man sollte sich von der TLA+-Sprache selbst nicht einschüchtern lassen, trotz des einschüchternden Namens ist der Zugriff auf ihre leistungsstarken Funktionen recht einfach. Tatsächlich könnte ein TLA+-Spickzettel, der fast alle TLA+-Funktionen beschreibt, ungefähr auf eine Seite passen:
mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
Darüber hinaus ist der Aufwand für die Erstellung des Modells vergleichbar mit standardmäßigen manuellen Sicherheitsüberprüfungen. Bei einem ckBTC-Minter würde es beispielsweise insgesamt etwa drei Wochen dauern, bis eine Person das Design versteht, das ursprüngliche Modell und die Eigenschaften erstellt.
Das resultierende TLA+-Modell ist viel einfacher als die Implementierung, sowohl weil es einfacher als Code ist, als auch wegen der High-Level-Natur von TLA+. Das Modell für den ckBTC-Minter erfordert etwa 250 Zeilen Code im Vergleich zu den Tausenden Zeilen der Rust-Implementierung. Es überrascht vielleicht, dass einer der schwierigsten Teile in Bezug auf den Aufwand die Spezifikation der erforderlichen Eigenschaften ist, da es in intuitiven Spezifikationen häufig Lücken gibt.
Sobald das Modell fertig ist, wird die Analyse (Modellprüfung) automatisch abgeschlossen. Die Ausführung der Analyse kann lange dauern – für ckBTC dauerte sie beispielsweise über 20 Stunden. Ein weiterer Vorteil von TLA besteht schließlich darin, dass Modellierung und Analyse bereits in der Entwurfsphase durchgeführt werden können, bevor der Code implementiert wird, was dazu beiträgt, spätere umfangreiche Umgestaltungen aufgrund von Entwurfsfehlern zu vermeiden.
Wobei TLA+ nutzlos ist
Negativ zu vermerken ist, dass TLA+ bei komplexen sequentiellen Programmen weniger hilfreich ist als bei gleichzeitigen Programmen, und es eignet sich auch nicht gut für den Umgang mit komplexen kryptografischen Protokollen, für die es andere Tools (z. B. Tamarin) gibt, die nützlicher sind.
Schließlich besteht noch das Problem, das TLA+-Modell und die tatsächliche Implementierung synchron zu halten, da sich der Implementierungscode im Laufe der Zeit weiterentwickelt und möglicherweise nicht mehr dem Modell entspricht, was ohne Toolunterstützung schwierig zu erkennen sein kann.
Tatsächlich versucht unser Forschungs- und Entwicklungsteam, dieses Problem zu lösen – ich hoffe, wir können bald einige Tools mit Ihnen teilen!
Ich hoffe, dieser Überblick hat Ihr Interesse an der Verwendung von TLA+ für Ihre eigenen kritischen Smart Contracts geweckt. Wenn ja, bleiben Sie auf dem Laufenden – in Kürze erscheint ein Folgebeitrag mit einem ausführlicheren Tutorial zur Verwendung von TLA+ für Smart Contracts. und Beigefügt ist ein tatsächliches TLA+-Modell, das von unserem Forschungs- und Entwicklungsteam entwickelt wurde.
IC-Inhalte, die Ihnen wichtig sind
Technologiefortschritt |. Projektinformationen |
Sammeln und folgen Sie dem IC Binance Channel
Bleiben Sie mit den neuesten Informationen auf dem Laufenden