Search

Software security becomes increasingly important nowadays. Security should be considered as early as possible in the software development. However, considering different aspects of security is a complex task. In this paper, we propose an extendable framework for continuous secure software development and evolution. The framework provides interconnected analyses on different stages of development. Explicit assumption management helps to verify the security requirements more properly. Thus, the security of the system under development can be estimated more accurately. Finally, the concrete assumptions also help to identify and close security gaps that arise during the software’s lifetime.

In this report, we present an approach for the quantification of correctness of service-oriented software systems by combining the modeling tool Palladio and the deductive verification approach KeY. Our approach uses Palladio for modeling the service-oriented architecture, the usage scenarios of the system (called services) in particular, and the distribution of values for the parameters provided by the users. The correctness of a service is modeled as a Boolean condition. We use Palladio to compute the probability of a service being called with critical parameters, i.e., in a way that its correctness condition is violated. The critical parameters are computed by KeY, a deductive verification tool for Java. The approach is not limited to KeY: Other techniques, such as bug finding (testing, bounded model checking) can be used, as well as other verification tools. We present two scenarios, which we use as examples to evaluate the feasibility of the approach. Finally, we close with remarks on the extension to security properties. Furthermore, we discuss a possible approach to guide developers to locations of the code that should be verified or secured.

Qualitätsmerkmale eines Software-Systems wie Zuverlässigkeit oder Performanz können über dessen Erfolg oder Scheitern entscheiden. Diese Qualitätsmerkmale können im klassischen Software-Ingenieurswesen erst bestimmt werden, wenn der Entwurfsprozess bereits vollendet ist und Teile des Software-Systems implementiert sind. Computer-Simulationen erlauben es jedoch Schätzungen dieser Werte schon während des Software-Entwurfs zu bestimmen. Simulationen werden erstellt um bestimmte Aspekte eines Systems zu analysieren. Die Repräsentation des Systems ist auf diese Analyse spezialisiert. Diese Spezialisierung resultiert oft in einer monolithischen Struktur der Simulation. Solch eine Struktur kann jedoch die Wartbarkeit der Simulation negativ beeinflussen und das Verständnis und die Wiederverwendbarkeit der Repräsentation des Systems verschlechtern. Die Nachteile einer monolithischen Struktur können durch das Konzept der Modularisierung reduziert werden. In diesem Ansatz wird ein Problem in kleinere Teilprobleme zerlegt. Diese Zerlegung ermöglicht ein besseres Veständnis und eine bessere Handhabung der Teilprobleme. In dieser Arbeit wird ein Ansatz präsentiert, um die Kopplung von neu entwickelten oder bereits existierenden Simulationen zu einer modularen Simulation zu beschreiben. Dieser Ansatz besteht aus einer Domänenspezifischen Sprache (DSL), die mit modellgetriebenen Technologien entwickelt wird. Die DSL wird in einer Fallstudie angewendet, um die Kopplung von zwei Simulationen zu beschreiben. Weiterhin wird die Kopplung dieser Simulationen mit einem existierenden Kopplungsansatz gemäß der erzeugten Beschreibung manuell implementiert. In dieser Fallstudie wird die Vollständigkeit der Fähigkeit der DSL untersucht, die Kopplung von mehreren Simulation zu einer modularen Simulation zu beschreiben. Weiterhin wird die Genauigkeit des Modularisierungsansatzes bezüglich der Verhaltensbewahrung der modularen Simulation gegenüber der monolithischen Version evaluiert. Hierfür werden die Resultate der modularen Simulation mit denen der monolithischen Version verglichen. Zudem wird die Skalierbarkeit des Ansatzes durch die Betrachtung der Ausführungszeiten untersucht, wenn mehrere Simulationen gekoppelt werden. Außerdem wird der Effekt der Modularisierung auf die Ausführungszeit in Relation zur monolithischen Simulation betrachtet. Die erhaltenen Resultate zeigen, dass die Kopplung der beiden Simulationen der Fallstudie, mit der DSL beschrieben werden kann. Die Resultate bezüglich der Evaluation der Genauigkeit weisen Probleme bei der Interaktion der Simulationen mit dem Kopplungsansatz auf. Nichts desto trotz bleibt das Verhalten der monolithischen Simulation in der modularen Version insgesamt erhalten. Die Evaluation zeigt, dass die modulare Simulation eine Erhöhung der Ausführungszeit im Vergleich zur monolithischen Version erfährt. Zudem deutet die Analyse der Skalierbarkeit darauf hin, dass die Ausführungszeit der modularen Simulation nicht exponentiell mit der Anzahl der gekoppelten Simulationen wächst.

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