Certora verifiziert offiziell Solanas P-Token-Upgrade als gleichwertig zum SPL-Token

Das kürzlich von Solana eingeführte P-Token-Upgrade stellt eine der bedeutendsten Infrastrukturänderungen in der Geschichte des Netzwerks dar. Das Upgrade reduziert die für Token-Operationen erforderlichen Rechenressourcen drastisch, während die Kompatibilität mit dem bestehenden SPL-Token-Programm erhalten bleibt.

Um diese Behauptung zu untermauern, beauftragte die Solana Foundation Certora mit der Durchführung einer formalen Verifizierung, um die Verhaltensäquivalenz zwischen der bestehenden SPL-Token-Implementierung und dem neuen Pinocchio-basierten P-Token-Programm nachzuweisen. Das Forschungs- und Entwicklungsunternehmen Anza hat die formale Verifizierung bereits als "stärkste Garantie" für die Gleichwertigkeit von P-Token bezeichnet, und die Ergebnisse von Certora sind eine weitere Bestätigung für die Rolle von P-Token als "Drop-in"-Ersatz für eines der am häufigsten verwendeten Programme von Solana.

Warum das Token-Programm so wichtig ist

Das SPL-Token-Programm steht im Zentrum der Token-Wirtschaft von Solana. Es wickelt die Erstellung von Münzen, die Verwaltung von Token-Konten, Übertragungen, Verbrennungen und Delegationen für die große Mehrheit der Vermögenswerte im Netzwerk ab. Da fast jede nicht stimmberechtigte Transaktion auf Solana in irgendeiner Form mit Token interagiert, hat jede Änderung am Token-Programm weitreichende Auswirkungen auf das Ökosystem.

P-Token führt eine neue Implementierung ein, die auf der Pinocchio Rust-Bibliothek basiert. Das Upgrade bringt erhebliche Leistungsverbesserungen mit sich und reduziert den Rechenaufwand für viele gängige Operationen um etwa 95-98 %. Standard-Token-Transfers fallen beispielsweise von 4.645 Recheneinheiten auf nur 76, während transfer_checked-Anweisungen von 6.200 Recheneinheiten auf 105 sinken.

Durch diese Effizienzgewinne können schätzungsweise 12-13 % des Blockraums im gesamten Netzwerk freigesetzt werden, wodurch zusätzliche Kapazität geschaffen wird, ohne die Blockgrenzen zu erhöhen.

Die Herausforderung, einen "Drop-In"-Ersatz zu beweisen

Während Leistungsverbesserungen die Aufmerksamkeit auf sich ziehen, bleibt die Kompatibilität die wichtigste Anforderung für ein Infrastruktur-Upgrade dieser Größenordnung. Bestehende Wallets, dApps, Protokolle und Smart Contracts sind auf das Verhalten des SPL Token-Programms angewiesen. Jede unerwartete Abweichung könnte zu Integrationsproblemen führen oder ein Risiko für Entwickler und Nutzer darstellen.

P-Token kopiert nicht einfach die ursprüngliche Codebasis. Die neue Implementierung verwendet eine andere Architektur, die unter anderem einen kopierfreien Kontozugriff, optimierte Ausführungspfade und zusätzliche Funktionen vorsieht. Daher konnten sich die Entwickler nicht allein auf herkömmliche Tests zur Feststellung der Kompatibilität verlassen.

Stattdessen verwendete Certora formale Verifikationstechniken, um mathematisch zu analysieren, ob sich die beiden Programme bei allen möglichen Eingaben innerhalb des definierten Verifikationsbereichs gleich verhalten.

Was bedeutet Äquivalenz für P-Token?

Der Verifikationsrahmen von Certora bewertet drei Ergebniskategorien für jede analysierte Anweisung.

• Erstens: Keines der beiden Programme darf während der Ausführung in Panik geraten, d.h. das Programm darf niemals abstürzen oder aufgrund eines Fehlers, eines Randfalls usw. abgebrochen werden.

• Zweitens: Wenn das SPL-Token-Programm eine Anweisung erfolgreich verarbeitet und Ok(()) zurückgibt, muss P-Token ebenfalls Ok(()) zurückgeben. In diesen Fällen müssen beide Programme die Kontodaten nach der Ausführung in einem Byte-für-Byte identischen Zustand hinterlassen.

• Drittens, wenn P-Token einen Fehler zurückgibt, muss das SPL-Token-Programm unter denselben Bedingungen denselben Fehler zurückgeben.

Das Certora-System stellt sicher, dass das Programm für jeden möglichen Kontostand und jede mögliche Anweisung entweder erfolgreich ist (Ok(()) oder ordnungsgemäß scheitert (Err(e)), aber niemals intern abstürzt. Die Implementierung von P-Token ist als Obermenge der SPL Token-Funktionalität konzipiert, d.h. jede von SPL Token akzeptierte Operation muss auch von P-Token akzeptiert werden.

Bei der Überprüfung wurden mehrere bewusste Unterschiede zwischen den beiden Programmen festgestellt. P-Token ermöglicht den Selbstwiderruf von Delegaten, d. h. ein Delegat kann seine eigene Autorität widerrufen, ohne dass der Token-Kontoinhaber die Transaktion unterzeichnen muss. Bei SPL Token ist für die gleiche Aktion die Unterschrift des Besitzers erforderlich.

P-Token erweitert außerdem die Unterstützung für Token-2022-Multisig-Autoritäten. Während SPL Token diese Konten ablehnt, akzeptiert P-Token sie.

Ein dritter Unterschied betrifft die Fehlerbehandlung, wenn fehlerhafte Kontodaten nicht-kanonische COption-Tags enthalten. SPL Token weist solche Konten sofort mit einem InvalidAccountData-Fehler zurück. Der optimierte Kontoladeprozess von P-Token greift tiefer in die Befehlslogik ein, bevor er einen Fehler erzeugt, was je nach ausgeführtem Befehl zu unterschiedlichen Ergebnissen führen kann.

Da diese Unterschiede beabsichtigt und dokumentiert waren, bezog Certora Annahmen in Teile des Verifikationsprozesses ein, um die Analyse auf die vereinbarte Kompatibilitätsgrenze zu konzentrieren.

Wie die Verifizierung ablief

Der Prover von Certora analysiert den Quellcode nach der Kompilierung in eine Low-Level-Zwischendarstellung. Die Ingenieure schreiben dann formale Spezifikationen unter Verwendung der Certora Verification Language for Rust, bekannt als CVLR.

Das Verifizierungssystem erstellt identische Kopien von Kontoinformationen und Befehlsdaten, so dass der Prover beide Programme unter den gleichen Bedingungen vergleichen kann. Unter Verwendung von Satisfiability Modulo Theories-Techniken bewertete das System alle möglichen Eingaben gleichzeitig, anstatt sich auf eine begrenzte Sammlung von Testfällen zu verlassen.

Der Anwendungsbereich umfasste alle Anweisungen, die SPL Token und P-Token gemeinsam haben, mit Ausnahme von AmountToUiAmount und UiAmountToAmount. Auch die drei neuen P-Token-spezifischen Befehle batch, unwrap_lamports und withdraw_excess_lamports wurden nicht geprüft.

Während des gesamten Prozesses generierte der Prover entweder einen Korrektheitsbeweis oder lieferte konkrete Gegenbeispiele, die die zu überprüfenden Verhaltensunterschiede aufzeigten.

Befunde und Ergebnisse

Certora berichtete, dass während der Verifizierung keine ausnutzbaren Schwachstellen auftraten. Die Analyse bestätigte, dass die Eigenschaften "Keine Panik" und "Äquivalenz bei Ok" für alle Anweisungen innerhalb des Anwendungsbereichs gelten, ohne dass zusätzliche Annahmen erforderlich sind. Die Eigenschaft Äquivalenz bei Fehler gilt auch für den gemeinsamen Befehlssatz, wenn die drei zuvor identifizierten absichtlichen Verhaltensunterschiede berücksichtigt werden.

Vor allem aber hat die Verifikation gezeigt, dass beide Programme, wenn sie erfolgreich dieselbe Eingabe verarbeiten, Byte für Byte identische Post-Operation-Account-Zustände erzeugen. Der Prozess machte auch deutlich, wie die formale Verifizierung Grenzfälle aufdecken kann, die bei herkömmlichen Tests möglicherweise übersehen werden.

Ein bedeutender Meilenstein für Solana Infrastructure

Die Verifizierungsergebnisse wurden kurz nach dem Einsatz von P-Token im Mainnet erzielt und geben zusätzliches Vertrauen in eine der folgenreichsten Infrastruktur-Upgrades von Solana.

Durch die Kombination von beträchtlichen Recheneinsparungen und formal verifizierter Verhaltensäquivalenz soll das Upgrade die Effizienz des Netzwerks verbessern, ohne die Anwendungen und Anlagen zu beeinträchtigen, die tagtäglich auf das Token-Programm angewiesen sind.

Lesen Sie mehr über SolanaFloor

Solana erhält endlich native Onchain-Abonnements, die Gehaltsabrechnung, KI-Agentenbudgets und wiederkehrende Rechnungen freischalten
Noble Mobile des ehemaligen US-Präsidentschaftskandidaten Andrew Yang übernimmt Helium Mobile - Was passiert mit $HNT?

Wie wird sich der $2T IPO von SpaceX auf Krypto auswirken?