Research Topics and Achievements
In the following account, we highlight selected research contributions that have been achieved within the scope of RA4 in the excellence cluster. These are: (a) adding accountability to distributed systems, (b) detecting traffic differentiations, (c) design and analysis of security protocols, (d) discovery and quantification of information leaks, (e) user privacy and anonymity, (f) protocols for efficient multimedia transmission, and (g) verifiably correct systems.
Accountability for Distributed Systems
Many distributed computing systems aggregate the resources of participants to provide a service that exceeds the capabilities of any one participant. Examples include federated systems (in which commercial providers cooperate to offer a ubiquitous service) and peer-to-peer systems (in which users cooperate to implement a service without dedicated infrastructure.) A problem is that the participants do not fully trust each other and often have competing interests. To address these challenges, Haeberlen et al. have developed PeerReview, an algorithm that ensures accountability in any distributed system that can be described as a collection of deterministic state machines. In PeerReview, each node maintains a tamper-evident log, which records all messages the node sends and receives as well as inputs and outputs of the application. Any node can request the log of another node j and independently determine whether i-has deviated from its expected behavior. To do this, i replays j's log using a reference implementation that defines i-'s expected behavior. By comparing the results of the replayed execution with those recorded in the log, PeerReview can detect observable Byzantine faults without requiring a formal specification of the system.
The approach taken by PeerReview is very general, but it requires that each node's actions be deterministic; otherwise, a different non-deterministic choice by a node and its reference implementation would be classified incorrectly as a fault. To overcome this limitation, Backes et al. have developed a technique that provides cryptographically strong, accountable randomness, called CSAR. Using CSAR, one can generate a pseudo-random sequence and a proof that the elements of this sequence up to a given point have been correctly generated, while future values in the sequence remain unpredictable. CSAR enables accountability for distributed systems that use randomized protocols. External auditors can check if a node has deviated from its expected behavior without learning anything about the node's future random choices. In particular, an accountable node does not need to leak secrets that would make its future actions predictable. CSAR is practical and efficient.
PeerReview has been applied to a variety of different systems. Haeberlen et al. applied it to a server-based network file system, a decentralized email system, and a large-scale content distribution system to two multi-player games, and to the Internet interdomain routing system.
Glasnost: Enabling Users to Detect Traffic Differentiation
Holding residential ISPs to their contractual or legal obligations of "unlimited service" or "network neutrality" is hard because their traffic management policies are opaque to end users and governmental regulatory agencies. Dischinger et al. have built and deployed Glasnost, a system that improves network transparency by enabling ordinary Internet users to detect whether their ISPs are differentiating between flows of specific applications. They identified three key challenges in designing such a system: (a) to attract many users, the system must have low barriers to use and generate results in a timely manner; (b) the results must be robust to measurement noise and avoid false accusations of differentiation, which can adversely affect ISPs' reputation and business; and (c) the system must include mechanisms to keep it up to date with the continuously changing differentiation policies of ISPs worldwide. Glasnost has been operational for over a year. More than 350,000 users from over 5,800 ISPs worldwide have used Glasnost to detect differentiation, validating many of the design choices. The data from individual Glasnost users can be aggregated to provide regulators and monitors with useful information on ISP-wide deployment of various differentiation policies.
Design and Analysis of Security Protocols and Programs using Zero-Knowledge Proofs
Security proofs of cryptographic protocols are known to be difficult, and work towards the automation of such proofs started soon after the first protocols were developed.
A major focus of our research in this area has been to develop novel analysis techniques for dealing with protocols that involve zero-knowledge proofs. Backes et al. have developed an abstraction of non-interactive zero-knowledge proofs in the applied pi-calculus and exemplified the abstraction’s applicability to real-world protocols by automatically verifying the secrecy, authenticity, and anonymity properties of the Direct Anonymous Attestation (DAA) protocol using ProVerif. The analysis took about two minutes. Backes et al. subsequently devised a novel type system for statically analyzing the security of protocols based on their abstraction of non-interactive zero-knowledge proofs. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. The type system-based analysis of DAA took less than three seconds. Finally, they developed a general technique for the automated verification of remote electronic voting protocols, which typically rely on zero-knowledge proofs to achieve the anonymity of voters.
A central challenge in the design of security protocols for modern applications is devising protocols that satisfy strong security properties. Ideally, the designer should only have to consider restricted security threats (e.g., honest-but-curious participants); automated tools should then strengthen the original protocols so that they withstand stronger attacks (e.g., malicious participants). Backes et al. have proposed a general technique for automatically strengthening protocols so that they stay secure even in the presence of compromised participants. The central idea is to automatically transform the original cryptographic protocols by adding non-interactive zero-knowledge proofs and let each participant prove that the messages sent to the other participants are generated in accordance to the protocol. They used the aforementioned type system for zero-knowledge proofs to automatically verify the security of the transformed protocols. In order to facilitate the devision of executable programs from high-level security specifications, a tool chain was developed for compiling abstract protocol specifications in the applied pi-calculus down to ML and to Java executable code (in submission).
User Privacy, Anonymity and Trust in Social Networks
Online social networks are now a popular way for users to connect, express themselves, and share content. Users in today's online social networks often post a profile, consisting of attributes like geographic location, interests, and schools attended. Such profile information is used on the sites as a basis for grouping users, for sharing content, and for suggesting users who may benefit from interaction.
On the one hand, not all users provide these attributes in practice. Mislove et al. thus aimed at answering the following question: given attributes for some fraction of the users in an online social network, can we infer the attributes of the remaining users? To answer this question, they have gathered fine-grained data from two social networks and tried to infer user profile attributes. They discovered that users with common attributes are more likely to be friends and often form dense communities, and proposed a method of inferring user attributes that is inspired by previous approaches to detecting communities in social networks. Their results show that certain user attributes can be inferred with high accuracy when given information on as little as 20% of the users. On the other hand, an increasing number of users prefer to minimize the posted information to users seeking sensitive information may want to remain largely anonymous in order to avoid being stigmatized or other negative repercussions. Hamerlik et al. have developed a novel P2P search infrastructure for providing anonymous and censorship-resistant content sharing. Backes et al. have furthermore proposed formal definitions and automated analysis techniques for sophisticated anonymity properties such as receipt-freeness and coercion-resistance in electronic voting protocols, as well as user anonymity in attestation protocols.
Mislove et al. have also investigated how to make use of trust relationships in order to block unwanted communication such as email spam, Web search engine spam, inappropriately labeled content on YouTube, and unwanted contact invitations in Skype. They have shown how to use trust relationships such as social links to thwart unwanted communication. Such relationships already exist in many application settings today. Their system, Ostra, bounds the total amount of unwanted communication a user can produce based on the number of trust relationships the user has, and relies on the fact that it is difficult for a user to create arbitrarily many trust relationships. Ostra does not rely on automatic classification of content, does not require global user authentication, respects each recipient's idea of unwanted communication, and permits legitimate communication among parties who have not had prior contact. In a complementary line of work, Backes et al. have shown how to achieve such trusted communications even in fully anonymous settings. Their system relies on zero-knowledge proofs that convince the recipient that a certain trust relationship holds, without divulging any other information such as the sender's identity.
Novel Schemes for Multimedia Transmission
Devising efficient protocols for multimedia transmission is particularly important for various low-bandwidth situations that arise within the scope of the excellence cluster. Li et al. have provided a wide area UMTS Release 5 (HSUPA)-based video streaming out of a moving car. During the period of three months a car has been driving throughout Germany, streaming video data several times per day to the internet browsers of community participants. The technology comprises communications (UMTS/HSUPA), broadcast (MPEG-2 Transport Stream incl. adaptive error correction) and internet technologies (H.264 multicast video streaming).
Tan et al. have furthermore developed an adaptive hybrid error correction scheme specifically targeted at multimedia transmission (streaming). This protocol is unique in the sense that it provides predictable reliability under predictable delay, a characteristic essential for multimedia data and not available in a mathematically-founded way today. The protocol enables wireless multicast video distribution as well as very efficient IP-based multimedia service delivery. It has been extensively published. The most recent work extended the protocol toward a multi-segment solution, so that typical streaming infrastructures (WAN, DSLAM, Home Gateway) can further be optimized by terminating the protocols in the routers. To prove the applicability of the new protocol, a DLNA (Digital Living Network Alliance) middleware stack has been implemented and the protocol has been incorporated for local wireless multicast Digital Television redistribution.
Verifiably Correct Systems
The Verisoft project is a long-term research project funded by the German Federal Ministry of Education and Research (bmb+f). Its goal is to develop theory and tools to come up with verifiably correct systems. It concentrates on the formal and pervasive computing of five concrete application tasks, one from an academic background (system for signed emails), and four from an industrial background (a biometric identification scheme, an automotive system, a 32bit-microcontroller, and parts of the software and system structure of a 'System-on-Chip' (SoC) from the mobile telephone sector). Computer-aided verification tools are used throughout all layers of abstractions. This way, human errors are excluded, full coverage is achieved, and the results are based on a well-known small set of assumptions. Hence, the verified systems are guaranteed to adhere to the high standards of quality required in many industrial sectors, such as automotive engineering, security, and medical technology. We list, as examples, two publications that arose from the Verisoft project. More information can be found on project's web page at www.verisoft.de.