Textdokument
Automatisierte Garantierte Blockchain-Technologie Verifizierung
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Zusatzinformation
Datum
2024
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
Blockchain-Technologien haben sowohl in der Wissenschaft als auch in der Industrie
große Aufmerksamkeit auf sich gezogen. Da sie als Mittel zum Halten und Manipulieren von
Finanzwerten verwendet werden, sind sie ein beliebtes Ziel von Angriffen. In der Vergangenheit
sind bereits Vermögenswerte in der Größenordnung von Millionen von US-Dollar verloren gegangen.
Vor diesem Hintergrund ist die Fähigkeit, sicherzustellen, dass keine Schwachstellen vorhanden
sind, von entscheidender Bedeutung. Die hier zusammengefasste Dissertation stützt sich auf die
jüngsten Fortschritte im Bereich der symbolischen Modellprüfung, insbesondere auf Techniken, die auf
Satisfiability Modulo Theories (SMT) und Constrained Horn Clauses (CHC) basieren, um den Bedarf
an einer automatisierten Überprüfung von Blockchain-Technologien zu decken. Der Blockchain-
Bereich wird sowohl auf der Plattform- als auch auf der Anwendungsebene durch TLA+-Spezifikationen
und Solidity-Smart-Contracts angegangen, und die Verwendung von Korrektheitszeugnissen zur
Zertifizierung der Ergebnisse von Solvern, die für die betreffenden Logikfragmente bestimmt sind,
wird als Mittel zur Gewährleistung der Korrektheit untersucht.