Declarative design and enforcement for secure cloud applications

Abstract

The growing demands of users and industry have led to an increase in both size and complexity of deployed software in recent years. This tendency mainly stems from a growing number of interconnected mobile devices and from the huge amounts of data that is collected every day by a growing number of sensors and interfaces. Such increase in complexity imposes various challenges -- not only in terms of software correctness, but also with respect to security. This thesis addresses three complementary approaches to cope with the challenges: (i) appropriate high-level abstractions and verifiable translation methods to executable applications in order to guarantee flawless implementations, (ii) strong cryptographic mechanisms in order to realize the desired security goals, and (iii) convenient methods in order to incentivize the correct usage of existing techniques and tools. In more detail, the thesis presents two frameworks for the declarative specification of functionality and security, together with advanced compilers for the verifiable translation to executable applications. Moreover, the thesis presents two cryptographic primitives for the enforcement of cloud-based security properties: homomorphic message authentication codes ensure the correctness of evaluating functions over data outsourced to unreliable cloud servers; and efficiently verifiable non-interactive zero-knowledge proofs convince verifiers of computation results without the verifiers having access to the computation input.

Die wachsenden Anforderungen von Seiten der Industrie und der Endbenutzer verlangen nach immer komplexeren Softwaresystemen -- größtenteils begründet durch die stetig wachsende Zahl mobiler Geräte und die damit wachsende Zahl an Sensoren und erfassten Daten. Mit wachsender Software-Komplexität steigen auch die Herausforderungen an Korrektheit und Sicherheit. Die vorliegende Arbeit widmet sich diesen Herausforderungen in Form dreier komplementärer Ansätze: (i) geeignete Abstraktionen und verifizierbare Übersetzungsmethoden zu ausführbaren Anwendungen, die fehlerfreie Implementierungen garantieren, (ii) starke kryptographische Mechanismen, um die spezifizierten Sicherheitsanforderungen effizient und korrekt umzusetzen, und (iii) zweckmäßige Methoden, die eine korrekte Benutzung existierender Werkzeuge und Techniken begünstigen. Diese Arbeit stellt zwei neuartige Abläufe vor, die verifizierbare Übersetzungen von deklarativen Spezifikationen funktionaler und sicherheitsrelevanter Ziele zu ausführbaren Cloud-Anwendungen ermöglichen. Darüber hinaus präsentiert diese Arbeit zwei kryptographische Primitive für sichere Berechnungen in unzuverlässigen Cloud-Umgebungen. Obwohl die Eingabedaten der Berechnungen zuvor in die Cloud ausgelagert wurden und zur Verifikation der Berechnungen nicht mehr zur Verfügung stehen, ist es möglich, die Korrektheit der Ergebnisse in effizienter Weise zu überprüfen.