PUB - Publikationen an der Universität Bielefeld

Ein Smart Contract ist ein auf der Blockchain basierendes Softwaresystem zur dezentralen und unveränderlichen Behandlung von Transaktionen.Aufgrund dieser zugrundeliegenden Unveränderlichkeit können Smart Contracts nach ihrer initialen Veröffentlichung nicht mehr modifiziert werden. Selbst Softwarefehler oder Sicherheitslücken können nicht im Nachhinein behoben werden. Um die Korrektheit und Sicherheit der Contracts vor der Veröffentlichung festzustellen, müssen statische Analysen verwendet werden.\r\nAufgrund der zugrundeliegenden Blockchain Technologie muss eine Funktion des Smart Contracts genutzt werden, um eine Variable zu modifizieren. Um Zugriffe auf diese Variablen auf Implementierungsebene einzuschränken, erweitern wir in dieser Arbeit den Ansatz von Reiche u. a., welcher Zugriffskontrollrichtlinien auf Architekturebene beschreibt und auf Implementierungsebene durchsetzt.\r\nDiese Arbeit setzt sich als Ziel, modellierte rollen-basierte Zugriffskontrollrichtlinen (RBAC) für Solidity Smart Contracts auf korrekte Weise auf Implementierungsebene zu erzwingen. Dazu erweitern wir das Standard RBAC Modell von Sandhu, Ferraiolo und Kuhn um unsichere Informationsflüsse zwischen Variablen und zusätzlichen Authorisierungseinschränkungen für Rollen. Um die daraus folgenden Richtlinien auf Architekturebene zu modellieren wird ein neues Metamodell entwickelt. Die so modellierten Richtlinien werden auf Implementierungsebene in formale Spezifikationen übersetzt, was die korrekte Umsetzung dieser gewährleistet. Diese Übersetzung wird automatisch in einem Generator implementiert. Um die generierte Implementierung anschließend zu überprüfen, werden Werkzeuge wie solc-verify und Slither angewendet und erweitert. Abschließend wird der Entwicklungsprozess skizziert, der sich aus diesem Ansatz ergibt.\r\nUm diesen Ansatz zu evaluieren, und so Probleme und Limitierungen aufzuzeigen, wird eine Fallstudie mithilfe der drei Smart Contract Systeme Augur, Fizzy und Palinodia durchgeführt. Zusätzlich wird eine Metamodel Coverage Analyse eingesetzt, um die Vollständigkeit des Metamodels zu verifizieren. Abschließend argumentieren wir für die korrekte Durchsetzung der modellierten Zugriffskontrollrichtlinien bei der Verwendung unseres Ansatzes.\r\nWie die Evaluation zeigt, kann eine korrekte Umsetzung garantiert werden, solange bestimmte Annahmen eingehalten und Informationsflüsse nicht betrachtet werden. Um dies weiter zu evaluieren wurden Verletzungen der zugrundeliegenden Richtlinien in die Fallstudie eingefügt. Der vorgestellte Ansatz findet 100% dieser händisch hinzugefügten Probleme. Zusätzlich wird gezeigt, dass das entwickelte Metamodel vollständig genug ist, um rollen-basierte Zugriffskontrollrichtlinen zu beschreiben. Außerdem enthält es keine unnötigen Elemente, da ungefähr 90% des Metamodels vom Generator abgedeckt werden. Lediglich bestimmte Limitierungen wie öffentliche Variablen oder die Verwendung von Orakeln wird nicht abgedeckt.

---

Master Thesis, KIT Karlsruhe, 2022