Security and Privacy by Declarative Design

The privacy of users has rapidly become one of the most pervasive and stringent requirements in distributed computing. Designing and implementing privacy-preserving distributed systems, however, is challenging since these systems also have to fulfill seemingly conflicting security properties and system requirements: e.g., authorization and accountability require some form of user authentication and session management necessarily involves some form of user tracking. In this work, we present a solution based on declarative design. The core component of our framework is a logic-based declarative API for data processing that exports methods to conveniently specify the system architecture and the intended security properties, and conceals the cryptographic realization. Invisible to the programmer, the implementation of this API relies on a powerful combination of digital signatures, non-interactive zero-knowledge proofs of knowledge, pseudonyms, and reputation lists. We formally proved that the cryptographic implementation enforces the security properties expressed in the declarative specification. The systems produced by our framework enjoy interoperability and open-endedness: they can easily be extended to offer new services and cryptographic data can be shared and processed by different services, without requiring any extra bootstrapping phase or interaction among parties. We implemented the API in Java and conducted an experimental evaluation to demonstrate the practicality of our approach.