Modelling and Enforcing Access Control Requirements for Smart Contracts

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.
Aufgrund der zugrundeliegenden Blockchain Technologie muss eine Funktion des Smart Contracts genutzt werden, um eine Variable zu modifizieren. ... mehrUm 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.
Diese 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.
Um 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.
Wie 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.

Smart contracts are software systems employing the underlying blockchain technology to handle transactions in a decentralized and immutable manner. Due to the immutability of the blockchain, smart contracts cannot be upgraded after their initial deploy. Therefore, reasoning about a contract’s security aspects needs to happen before the deployment. One common vulnerability for smart contracts is improper access control, which enables entities to modify data or employ functionality they are prohibited from accessing. Due to the nature of the blockchain, access to data, represented through state variables, can only be achieved by employing the contract’s functions. ... mehrTo correctly restrict access on the source code level, we improve the approach by Reiche et al. who enforce access control policies based on a model on the architectural level.
This work aims at correctly enforcing role-based access control (RBAC) policies for Solidity smart contract systems on the architectural and source code level. We extend the standard RBAC model by Sandhu, Ferraiolo, and Kuhn to also incorporate insecure information flows and authorization constraints for roles. We create a metamodel to capture the concepts necessary to describe and enforce RBAC policies on the architectural level. The policies are enforced in the source code by translating the model elements to formal specifications. For this purpose, an automatic code generator is implemented. To reason about the implemented smart contracts on the source code level, tools like solc-verify and Slither are employed and extended. Furthermore, we outline the development process resulting from the presented approach.
To evaluate our approach and uncover problems and limitations, we employ a case study using the three smart contract software systems Augur, Fizzy and Palinodia. Additionally, we apply a metamodel coverage analysis to reason about the metamodel’s and the generator’s completeness. Furthermore, we provide an argumentation concerning the approach’s correct enforcement.
This evaluation shows how a correct enforcement can be achieved under certain assumptions and when information flows are not considered. The presented approach can detect 100% of manually introduced violations during the case study to the underlying RBAC policies. Additionally, the metamodel is expressive enough to describe RBAC policies and contains no unnecessary elements, since approximately 90% of the created metamodel are covered by the implemented generator. We identify and describe limitations like oracles or public variables.