Text Document
Automatisierte Garantierte Blockchain-Technologie Verifizierung
No Thumbnail Available
Fulltext URI
Document type
Additional Information
Date
2024
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Gesellschaft für Informatik e.V.
Abstract
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.