Universität Stuttgart
Permanent URI for this communityhttps://elib.uni-stuttgart.de/handle/11682/1
Browse
Search Results
Item Open Access Implementierung und Sicherheitsanalyse von High Mountain Range Options auf einer Blockchain(2018) Bechtold, MarvinKryptowährungen auf Basis von Blockchaintechnologie haben in den letzten Jahren immer mehr an Bedeutung und Verbreitung gewonnen. In vielen unterschiedlichen Geschäftsfeldern forschen und arbeiten Unternehmen am Einsatz dieser Technologie, um neue oder disruptive Prozesse oder gar Geschäftsmodelle zu entwickeln. Voraussetzung ist die Nutzung der richtigen Blockchain und die Entwicklung entsprechender Smart Contracts. Die Smart Contracts sollen einfache, aber auch zunehmend komplexe Sachverhalte abbilden und dabei die herkömmliche Vertrauensinstanz durch die Blockchain ersetzen. Die Anforderung an Smart Contracts ist hierbei nicht nur die korrekte Abwicklung des Sachverhalts, sondern auch, ein hohes Maß an Sicherheit zu gewährleisten. In dieser Arbeit werden eine komplexe Aktienoption aus der Gruppe der High-Mountain-Range-Optionen und ihre Prozesse wie Erstellung, Kauf und Auszahlung durch Smart Contracts abgebildet. Als Blockchainframework wurde Hyperledger Fabric verwendet. Um die Arbeit verständlicher zu machen, wurde der fachliche Hintergrund von Aktienoptionen erörtert und die Funktionsweise der Blockchain dargestellt. Durch die Implementierung einer komplexen High Mountain Range Option wurde aufgezeigt, dass beliebige Aktienoptionen, von einfachen Aktienoptionen bis hin zum komplexen Finanzderivat, mittels Smart Contracts und Blockchain abgebildet werden können. Zusätzlich wurde die Sicherheit der implementierten Smart Contracts analysiert. Dabei wurde das Analysetool Chaincode Scanner verwendet. Die Ergebnisse geben Hinweise auf mögliche Schwachstellen, die bei der Implementierung von Smart Contracts berücksichtigt werden sollten.Item Open Access Übersicht über das Hacker-Ökosystem(2018) Geyer, SimonIn einer zunehmend vernetzten Welt nimmt Informationstechnologie eine zentrale Rolle in der Gesellschaft ein. Daher haben Hacker, als Angreifer auf IT-Systeme, einen starken und teils gefährlichen Einfluss auf die Gesellschaft. Diese Arbeit verfolgt das Ziel, anhand von Technologien und existierender Literatur einen Überblick über das Hacker-Ökosystem zu erstellen. Dabei wird zunächst auf Angreifer selbst und eine mögliche Klassifikation eingegangen. Daraufhin werden relevante Aktivitäten von Angreifern thematisiert. Davon ausgehend werden wirtschaftliche Aspekte wie der Handel auf Untergrundmärkten zwischen Hackern erläutert. Dazu wird auf Kryptowährungen wie Bitcoin und deren technische Funktionsweise eingegangen. Ferner werden die Auswirkungen von Angriffen auf IT-Systeme diskutiert. Zum Abschluss wird auf Darknets sowie Anonymisierungstechnologien eingegangen. In diesem Kontext wird die Funktionsweise der beiden Technologien Tor und I2P näher erläutert.Item Open Access An expressive formal model of the web infrastructure(2018) Fett, Daniel; Küsters, Ralf (Prof. Dr.)The World Wide Web is arguably the most important medium of our time. Billions of users rely on the security of the web each day for tasks such as banking, shopping, and business and private communication. The web is a heterogeneous infrastructure developing at a high pace. The question of whether the web infrastructure or certain web applications are secure is not easy to answer. Standards and applications today are reviewed by experts before they are deployed, but all too often even serious security vulnerabilities are simply overlooked. In this thesis, we propose a formal model for the web infrastructure which enables a rigorous formal analysis of security and privacy in the web. Our model is the most comprehensive and expressive model of the web infrastructure to date. It facilitates accurate security and privacy analyses of current web standards and applications, and can serve as a reference for web security researchers, developers of new technologies and standards, and for teaching web security concepts. As a case study we analyze the security of two important standards for federated authorization and authentication, OAuth 2.0 and OpenID Connect. Standardized by the IETF and OpenID Foundation, respectively, they are among the most widely deployed single sign-on systems in the web. For our analysis, we develop detailed formal models for both systems based on our model of the web infrastructure. These models then allow us to precisely define the security goals of authentication, authorization and session integrity. While proving security with respect to these goals, we found a total of five new attacks on the two single sign-on systems, breaking all of the security goals. In particular OAuth 2.0 had been analyzed many times before; the fact that we were able to find new attacks in OAuth 2.0 demonstrates the potential of rigorous analyses in our web infrastructure model. We develop fixes against the underlying vulnerabilities and are then able to prove the security of OAuth 2.0 and OpenID Connect. Since our results are based on a comprehensive model, our proofs can exclude large classes of attacks against OAuth and OpenID Connect, including yet unknown attack vectors. Our attacks and fixes led to the development of new security recommendations by the standardization organizations.Item Open Access Security analysis of the OpenID financial-grade API(2018) Hosseyni, PedramThe OpenID Financial-grade API provides a mechanism for accessing data and resources that need a high degree of protection, such as in the context of financial applications. As a profile of the OAuth 2.0 Authorization Framework designed for high-risk scenarios, the Financial-grade API aims at being secure even if the procedure is attacked at several points leading to wrongly configured endpoints, the leakage of tokens and even whole requests and responses. To achieve this degree of security, several additional mechanisms are used, which protect against the usage of leaked tokens and protect messages against modification. We modeled both the Read-Only Profile and the Read-Write Profile of the Financial-grade API in the FKS Web Model, including all underlying assumptions that might affect the security of the flows. Through formal analysis, we discovered several attacks not only on mechanisms specific to the Financial-grade API but also on more general concepts of OAuth, namely, Token Binding and the Proof Key for Code Exchange extension. We provide mitigations against these attack scenarios and show that the modified flows are secure as specified by our security definitions. More precisely, these modified flows prevent an attacker from logging in under the identity of an honest user and accessing protected resources belonging to the honest user.Item Open Access Implementation-level analysis of cryptographic protocols and their applications to e-voting systems(2018) Scapin, Enrico; Küsters, Ralf (Prof. Dr.)Formal verification of security properties of both cryptographic operations, such as encryption, and protocols based on them, such as TLS, has been the goal of a substantial research effort in the last three decades. One fundamental limitation in the verification of these security properties is that analyses are typically carried out at the design level and hence they do not provide reliable guarantees on the implementations of these operations/protocols. To overcome this limitation, in this thesis we aim at establishing formally justified cryptographic guarantees directly at the implementation level for systems that are coded in Java and use cryptography. Our approach is based on a general framework for the cryptographic verification of Java programs (the CVJ framework) which formally links cryptographic indistinguishability properties and noninterference properties. In this way, it enables existing tools that can check standard noninterference properties, but a priori cannot deal with cryptography, to also establish cryptographic privacy properties for Java systems. The CVJ framework is stated and proven for a Java-like formal language which however does not cover all the data types and features commonly used in Java programs. Moreover, the framework originally supports only one cryptographic operation, namely public-key encryption. The first contribution of this thesis is hence to extend and to instantiate the CVJ framework in order to make it more widely applicable. We extend the underlying formal language with some features of Java which have not been captured yet, such as concurrency, and we restate and prove all the results of the framework to carry them over into this extended language. We then further instantiate the framework with additional cryptographic operations: digital signatures and public-key encryption, both now also including a public-key infrastructure, (private) symmetric encryption, and nonce generation. The methods and techniques developed within the CVJ framework are relevant and applicable independently of any specific tool employed. However, to illustrate the usefulness of this approach, we apply the framework along with two verification tools for Java programs, namely the fully automated static checker Joana and the interactive theorem prover KeY, to establish strong cryptographic privacy properties for systems which use cryptography, such as client-server applications and e-voting systems. In this context, the second major contribution of this thesis is the design, the implementation, and the deployment of a novel remote voting system called sElect (secure/simple elections). sElect is designed to be particularly simple and lightweight in terms of its structure, the cryptography it uses, and the user experience. One of its unique features is a fully automated procedure which does not require any user interaction and it is triggered as soon as voters look at the election result, allowing them to verify that their vote has been properly counted. The component of sElect which provides vote privacy is implemented in Java such that we can establish cryptographic guarantees directly on its implementation: by combining the techniques of the CVJ framework with a hybrid approach for proving noninterference, we are able to show that the Java implementation ensures strong cryptographic privacy of the votes cast with our proposed voting system. sElect is therefore the first full-fledged e-voting system with strong cryptographic security guarantees not only at the design level, but also on its implementation.Item Open Access Analyse der Android-Sicherheitsarchitektur(2018) Krug, CarolaAndroid ist eine weit verbreitete Plattform für mobile Geräte, die nach Googles eigener Aussage von über zwei Milliarden Geräten genutzt wird. Dies verlangt nach einem ausreichenden Schutz der Gerätefunktionen und der Daten der Benutzer. Aus diesem Grund wird in dieser Arbeit die Android-Sicherheitsarchitektur analysiert. Nach einer kurzen Einführung zur Android-Architektur und einer Übersicht der Sicherheitskonzepte geht die Arbeit vor allem auf die Sicherheit des Linux-Kernels, SELinux und Permissions ein. Auch die Binder-Interprozesskommunikation wird näher erläutert. Der Linux-Kernel setzt dabei eine benutzerbasierte Prozessisolation und Zugriffskontrolle um. Dieser Mechanismus wird durch SELinux erweitert, wodurch die Möglichkeit besteht, Zugriffsrechte genauer zu definieren. Zur Zugriffskontrolle werden außerdem Permissions genutzt, die in verschiedene Sicherheitsstufen eingeteilt werden. Auf deren Zustimmung hat der Benutzer abhängig von der Sicherheitsstufe einen Einfluss. Trotz Prozessisolation müssen Prozesse miteinander kommunizieren können. Dazu ist in Android ein eigener Mechanismus, Binder, implementiert, der Nachrichten zwischen Prozessen über den Kernel leitet. Durch die Analyse dieser Komponenten der Android-Sicherheitsarchitektur wird verdeutlicht, wie Prozesse gegeneinander abgeschottet werden, der Zugriff auf Ressourcen gesteuert wird und trotz Prozessisolation eine sichere Kommunikation zwischen Prozessen möglich ist.Item Open Access Analysis of attacks on content security policies(2018) Schneider, TobiasCross-site scripting attacks are a major threat to web applications. Such attacks are used to inject undesirable content into web pages. The Content Security Policy is an approach to mitigate content injection and secure websites. The security mechanism is added to the HTTP header and prohibits the execution of inline scripts, whitelists resources and bans dangerous JavaScript functions. CSP is a client side protection and is enforced by the browser. The real-world adoption of the Content Security Policy is investigated due to the promising protection of CSP against cross-site scripting, having an adoption rate of 2.5% for the one million most popular sites in 2018. Unfortunately, the effort to make websites CSP compatible is high and results in a trade-off between security and functionality. Additionally, the security of CSP against content injection cannot keep its promises. In literature 94.72% of all investigated real-world policies are bypassed due to unsafe endpoints in the whitelist and other vulnerabilities. Finally, these numbers require changes in the use and concept of CSP.Item Open Access Nicht-interaktive Zero-Knowledge Beweise von Wissen mittels Fiat-Shamir Transformation(2018) Liedtke, JulianSigma-Protokolle sind sehr effiziente Beweise von Wissen. Leider weisen sie nur die Special Honest Verifier Zero-Knowledge Eigenschaft auf, welche schwächer als die Zero-Knowledge Eigenschaft ist. Das liegt daran, dass bei Honest Verifier Zero-Knowledge nur für ehrliche Verifizierer ein Simulator existieren muss, während bei Zero-Knowledge auch für bösartige Verifizierer, das sind Verifizierer, die sich möglicherweise nicht an das Protokoll halten, eine erfolgreiche Simulationen verlangt werden. Eine Möglichkeit, Sigma-Protokolle in Zero-Knowledge Protokolle umzuwandeln, besteht in der Fiat-Shamir Transformation. Dabei entsteht nicht nur ein Zero-Knowledge Beweis von Wissen, sondern auch ein nicht-interaktives Beweissystem. Die Idee der Fiat-Shamir Transformation besteht darin, dass der Beweiser die Challenge mittels einer Hashfunktion aus dem gemeinsamen Eingabewort und dem Commitment berechnet. Trotz der aktiven Verwendung der Fiat-Shamir Transformation in der Praxis wurde erst 2012 in Arbeiten von Bernhard, Pereira und Warinschi sowie Faust, Kohlweiss, Marson, und Venturi der Versuch eines Beweises der Korrektheit erbracht. Der Beweis der ersten Arbeit wird in dieser Masterarbeit ausformuliert.Item Open Access Über die (Un-)Sicherheit des W3C-WebAuthentication-Entwurfs: Eine Beschreibung und Sicherheitsanalyse(2018) Stötzner, MilesViele Dienste im Internet authentifizieren ihre Nutzer aufgrund der Benutzerfreundlichkeit durch ein Passwort. Dieses Passwort kann leicht von einem Angreifer in Erfahrung gebracht werden. Eine Lösung für dieses Problem ist der Einsatz mehrerer Faktoren. WebAuthentication (WebAuthn) ist ein Entwurf eines Standards, der auf eine benutzerfreundliche Weise einem Nutzer ermöglicht, sich bei einer Relying Party mithilfe eines asymmetrischen Schlüsselpaares durch das Signieren einer von der Relying Party generierten Nonce, die sogenannte Challenge, unter Einsatz von mehreren Faktoren passwortlos zu registrieren und authentifizieren. Während einer Registrierung oder Authentifizierung ist jeweils eine Relying Party, ein WebAuthn Client und ein Authenticator beteiligt. Der Authenticator ist für das Generieren des asymmetrischen Schlüsselpaares und für das Bereitstellen von Signaturen zuständig. Dabei muss jede Aktion von dem Nutzer autorisiert werden. Der WebAuthn Client befindet sich zwischen der Relying Party und dem Authenticator und ist für die Authentifizierung der Relying Party zuständig, sodass keine Aktion im Namen einer anderen Relying Party durchgeführt werden kann. Hierfür wird ein sicherer Kontext benötigt - d.h. die Verbindung ist über HTTPS gesichert. Während einer Registrierung wird ein asymmetrisches Schlüsselpaar generiert, dessen öffentlicher Schlüssel bei der Relying Party hinterlegt wird. Indem eine Signatur über die Challenge mit dem zugehörigen privaten Schlüssel generiert wird, kann sich ein Nutzer daraufhin authentifizieren. Teil dieser Arbeit ist eine Implementierung einer Relying Party, die WebAuthn für die Authentifizierung ihrer Nutzer verwendet. Hierfür betrachten wir neben der Implementierung eines Severs die Verwendung der WebAuthentication API. In einer informellen Sicherheitsanalyse untersuchen wir die Sicherheit des Protokolls, indem wir aufführen, wieso die während einer Registrierung bzw. Authentifizierung durchzuführenden Überprüfungen der einzelnen Parteien notwendig sind und welche Auswirkungen das Verwenden verschiedener Optionen von WebAuthn hat. Des Weiteren untersuchen wir die Kommunikationskanäle im Hinblick auf einen Man-in-the-Middle (MitM) und welche Gefahr von diesem ausgeht. Während der Sicherheitsanalyse betrachten wir einen Angriff auf das Authentifizierungsverfahren und widerlegen die in der Spezifikation aufgeführte Behauptung, dass WebAuthn während einer Registrierung resistent gegenüber einem MitM sei, der den sicheren Kontext ignorieren kann. Beide Probleme wurden von den Autoren der Spezifikation anerkannt. Für den Angriff auf das Authentifizierungsverfahren wurde bereits eine Lösung gefunden. Wir diskutieren, wieso das Authentifizierungsverfahren (nach Beheben unseres Angriffes) unter bestimmten Annahmen sicher ist und verweisen auf Probleme bezüglich der Privatsphäre und der für eine Registrierung oder Authentifizierung notwendige Zustimmung eines Nutzers. Zu den Annahmen zählen, dass der WebAuthn Client und Authenticator des Nutzers sowie die Relying Party sich konform verhalten, dass die Verbindung zwischen WebAuthn Client und Authentictor sicher ist und dass während der Registrierung kein erfolgreicher Angriff stattgefunden hat.Item Open Access Logistikprozess als Ethereum Smart Contracts : Implementierung und Sicherheitsanalyse(2018) Wangler, ThomasThemen rund um die Blockchain-Technologie haben in den letzten Jahren enorm an Aufmerksamkeit gewonnen. Neben dem populäreren Verwendungszweck als reine Kryptowährung entwickelte sich zusätzlich das Konzept Smart Contracts zur transparenten Abwicklung und Modellierung von Transaktionsprozessen, ohne gegenseitiges Vertrauen unter den beteiligten Parteien vorauszusetzen. Logistikprozesse im Rahmen des viel erforschten Themas Supply-Chain-Management stellen dabei eine Art von Transaktionsprozessen dar, welche bisher mindestens einseitiges Vertrauen von einer der beteiligten Parteien benötigten. Als eine zielführende Lösung dieser Problematik beschäftigt sich diese Bachelorarbeit daher mit der Implementierung eines Logistikprozesses auf Basis von Smart Contracts auf der Blockchain-Plattform Ethereum. Hierfür wurden diverse Smart Contracts, basierend auf einem Escrow-Verfahren, entwickelt, welche eine vollständige Modellierung des Prozesses eines Produktverkaufes und dessen Versand erlaubt. Im Rahmen der Implementierung wurde darauf geachtet, dass diese nicht anfällig gegenüber bekannten Sicherheitslücken von Ethereum Smart Contracts ist. Zusätzlich wurden im Zuge einer Sicherheitsanalyse alle Smart Contracts mit dem Analysetool OYENTE gegen diverse gängige Angriffsvektoren überprüft. DieseArbeit zeigt eine konkrete Möglichkeit auf, Logistikprozesse mittels Smart Contracts abzuwickeln und kann somit als potentielle Grundlage für weitere Smart Contract Logistikprozessmodellierungen verwendet werden.